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