Emanuele D'Osualdo

Researcher in Computer Science


The focus of my 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 for concurrent systems.

PhD Thesis

Verification of Message Passing Concurrent Systems
University of Oxford, 2015
Supervisor: Prof. C.-H. Luke Ong

My dissertation is concerned with the development of fully-automatic methods of verification, for message-passing based concurrent systems. In the first part of the thesis we define a sound parametric analysis framework for Erlang which exploits infinite‑state model checking to prove unreachability of error states, mutual exclusion, and bounds on mailboxes. The verification method is implemented in the prototype Soter. The second part of the thesis focusses on analyses for the π‑calculus. The outcome of this study is a type system, implemented in the tool James Bound, able to capture and check properties of the evolution of communication topology of a π‑term.

Winner of the 2016 CPHC/BCS Distinguished Dissertation award

Read More ORA Record Prototype tools

Selected Publications • See all

See all publications