December 15, 2016
Emanuele D'Osualdo
In this talk I will give an overview of my current research. The focus is on automatic analysis for message passing based concurrent systems, with an emphasis on dynamic communication topologies, i.e. systems where the components can connect and disconnect with each other dynamically. The distinctive trait of our approach to this problem is that the methods make full use of both, the structure of the programs as terms in a language, and the graph structure of the communication topology. This point of view unlocks the fruitful interaction of techniques from process algebra, type systems, automata theory and logics. I will present in some detail part of my PhD thesis work, which resulted in the type-theoretic definition of a fragment of the pi-calculus for which safety properties can be proved automatically. The types use novel techniques to reason about the shape that the communication topology can take at runtime. I will then give a brief account of ongoing projects pushing the approach further. The theme underlying all these projects is studying concurrent systems by analysing dynamic graphical structures capturing some salient aspect of their behaviour.