Abstract
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.