Formal methods for modeling and analysis of concurrent and distributed systems, in
particular models based on process calculi and automata. Study of expressiveness of such models and of analysis techniques based on type systems or behavioral equivalences. These techniques are applied in particular in the areas below:
- Reversible computing: in reversible computing it is possible to go back to previous states. Study of mechanisms for controlling reversibility, with the aim of exploiting reversibility for system recovery after a fault. Application of reversibility to debugging, in particular of programs written in the Erlang language, and to low-power computing.
- Quantum computing: techniques to model quantum protocols, and analysis to ensure their correctness properties.
- (Micro)Service-oriented computing: study of models for
(micro)service-oriented computing. Focus on the
programming language Jolie, in
collaboration with ItalianaSoftware s.r.l.
- Multiparty sessions: study of interactive systems based on
multiparty sessions. Study of specification languages for this kind
of systems, in particular for systems with dynamic join and leave
of participants, and study of techniques for realizing
services/components compatible with the specification.
