Overview

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.

Full Product Details

9781780173634

Table of Contents

Reviews

Author Information

Emanuele D'Osualdo studied for his PhD in the Department of Computer Science at the University of Oxford, under the supervision of Professor C. H. Luke Ong. Previously he obtained a B.Sc. and M.Sc. in Computer Science from the University of Udine, Italy. He is currently a postdoctoral researcher in the Concurrency Theory Group at the University of Kaiserslautern, Germany. His research interests are in concurrency theory and infinite-state verification, combining the approaches of semantics, process algebra, and automata theory. The focus of his research is finding models of concurrent behaviour with both theoretical and practical relevance: models that can deepen our understanding of computational phenomena and at the same time enable the construction of automatic analyses.

Tab Content 6

Countries Available