Specification and analysis of communication protocols

The course provides an overview of the application of formal methods to the specification and analysis of communication protocols in distributed systems. It introduces mathematical models and languages for describing process interactions, with particular emphasis on formal reasoning and the verification of key properties in relevant application domains such as the analysis of smart contracts and of robotics systems.

References and material

Lecture notes:

Further readings:

• [1] K. Honda, N. Yoshida and M. Carbone. Multiparty Asynchronous Session Types. JACM 63(1), 2016.
• [2] R. Kuhn, H. C. Melgratti and E. Tuosto. Behavioural Types for Local-First Software. ECOOP 2023
• [3] R. Kuhn, H. C. Melgratti and E. Tuosto. Behavioural Types for Local-First Software (Artifact). Dagstuhl Artifacts Ser. 2023
• [5] C. Fournet and G. Gonthier. The Reflexive CHAM and the Join-Calculus. POPL’96
• [6] A. J. Turon, C. V. Russo. Scalable join patterns. SPLASH 2011
• [7] Gul Agha. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, MA, USA, 1986.
• [7] D. Brand and P. Zafiropulo. On Communicating Finite-State Machines. JACM, 30(2):323–342, 1983.
• [8] P. Deniélou and N. Yoshida. Multiparty session types meet communicating automata. In ESOP 2012.
• [9] C. Hewitt, P. B. Bishop, and R. Steiger. A Universal Modular ACTOR Formalism for Artificial Intelligence. IJCAI, 1973.