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.
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
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
• See all
See all publications