Verification of Message Passing Concurrent Systems

As our world keeps delegating more and more critical tasks to networks of interconnected machines, developing astrong theoretical framework for their design and analysis is of paramount importance. This dissertation is concernedwith the development of fully-automatic methods of verification for message-passing based concurrent systems.First, we define a sound parametric analysis for Erlang, an industrial strength programming language. Thanks to acombination of abstraction and infinite-state model checking, our prototype implementation, called Soter, is able toprove properties of Erlang programs such as unreachability of error states, mutual exclusion, or bounds on mailboxes.The resulting analysis, however, has a blind spot: it is not able to precisely represent reconfigurable systems, i.e.systems where the communication network changes over time. To fix this, the second part of the thesis develops anovel type system for the analysis of the communication topology of pi-calculus processes.