On partial-order and automata techniques for analyzing communication

Message-passing is a key synchronization feature for concurrent programming and distributed systems.  In this model, processes running asynchronously synchronize by exchanging messages over unbounded channels.  The usual semantics is based on peer-to-peer communication, which is very popular for reasoning about telecommunication protocols. More recently, mailbox communication received increased attention because 
of its usage in multi-thread programming, as provided by languages like Rust or Erlang.

The talk will first survey results on verification and synthesis for peer-to-peer communication. 
In the second part we discuss recent work on mailbox communication and perspectives for synthesis.