I work in the field of Formal Methods for the verification of software.
I focused on two main approaches:
automatic verification methods using static analysis and infinite-state model checking;
and compositional methods, focusing on program logics for
properties beyond safety.
• See all
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