Publisher's Synopsis
As our world keeps delegating more and more critical tasks to networks of interconnected machines, developing a strong theoretical framework for their design and analysis is of paramount importance. This dissertation is concerned with 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 a combination of abstraction and infinite-state model checking, our prototype implementation, called Soter, is able to prove 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 a novel type system for the analysis of the communication topology of pi-calculus processes.
