• Contrast Style 4
  • Contrast Style 3
  • Contrast Style 2
  • Contrast Style 1
Text size

Verification of Message Passing Concurrent Systems

Emanuele D’Osualdo (author)

UK Price: £75.00 EU Price: €95.00 ROW (USD) Price: $105.00 
add to basket

Buy this eBook

BCS eBooks are available in a variety of formats, including Kindle, ePub and PDF. You can purchase this title from a number of online retailers (including those listed below).

ISBN: 9781780173634
Format: Paperback
Dimensions: 210 x 297 x 10
Number of pages: 206
Publication date: 21 NOV 2016
Publisher: BCS, The Chartered Institute for IT

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

Add a review

Post a review

Reviews are subject to approval by the moderator

Your Name *

Your Email Address (Not Published) *

Your Comments *


Please type the character "V" *

* = required field