I am Professor at the University of Surrey and a Director of the UK Research Institute on Verified Trustworthy Software Systems (VeTSS).
My research is on formal techniques and verification methods for concurrent and
real-time systems. This includes concurrent objects, transactional memory and associated correctness conditions; weak memory
models; algebraic
techniques; and hybrid systems.
I received a BSc in Computer Science and Mathematics and a BSc
(Hons) in Logic and
Computation, both from Victoria University of Wellington, New
Zealand. In 2009, I completed a PhD on
formal derivations of concurrent algorithms at the University
of Queensland, Australia. After this, I held postdoctorate positions at
the University of Queensland and then at the University of Sheffield. I was lecturer at Brunel University London from 2014-18 before joining Surrey as senior lecturer.
20/12/23: Paper accepted to ESOP 2024: Intel PMDK Transactions: Specification and Concurrency.
11/10/23: Paper accepted to VMCAI 2024: A Fully Verified Persistency Library.
08/09/23: New CHIST-ERA funded proposal: A Next-generation State-machine Replication Protocol for Blockchain.
18/08/23: Paper accepted to SEFM 2023: Verifying Read-Copy Update under RC11.
11/04/23: Paper accepted to CAV 2023: Rely-Guarantee Reasoning for Causally Consistent Shared Memory.
11/04/23: New EPSRC project funded: SACRED-MA: Safe And seCure REmote Direct Memory Access.
14/02/23: New EPSRC project funded: Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT).
05/01/23: Paper accepted to ACM Formal Aspects of Computing: Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies.
2022
20/12/22: Paper accepted to ACM WiSec 2023: Verifying List Swarm Attestation Protocols.
13/12/22: Paper accepted to ACM SAC-SVT 2023: Ownership-Based Owicki-Gries Reasoning.
15/11/22: Paper accepted to FM 2023: Reasoning about Promises in Weak Memory Models with Event Structures.
04/10/22: Paper accepted to FTSCS 2022: Proving Memory Access Violations in Isabelle/HOL.
30/06/22: Our paper on Implementing and Verifying Release-Acquire Transactional Memory in C11 has been accepted to OOPSLA 2022.
27/06/22: Our paper on Weak Progressive Forward Simulation is Necessary and Sufficient for Strong Observational Refinement has been accepted to CONCUR 2022.
17/05/22: Our paper on Modularising Verification Of Durable Opacity has been accepted to Logical Methods in Computer Science journal.
16/05/22: Our paper on Unifying Operational Weak Memory Verification: An Axiomatic Approach has been accepted to ACM Transactions in Computation Logic journal.
07/04/22: Our work on View-Based Owicki-Gries Reasoning for Persistent x86-TSO won a Distinguished Artifact award at ESOP 2022.
02/03/22: I will be joining the Editorial Board of Formal Aspects of Computing.
2021
11/11/21: I will be joining the Program Committee of iFM 2022.
04/10/21: Our paper on A Survey of Practical Formal Methods for
Security has been accepted for the Formal Aspects of Computing Journal.
27/09/21: Our paper on Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL has been accepted for the Journal of Automated Reasoning.
25/09/21: Our paper on Checking Opacity and Durable Opacity with FDR has been accepted for SEFM 2021.
23/07/21: Our brief announcement has been accepted to DISC 2021: Brief Announcement: On Strong Observational Refinement and
Forward Simulation.
17/07/21: Two papers have been accepted to Formal Methods 2021: Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies and Verifying Secure Speculation in Isabelle/HOL.
18/06/21: Our edited book on on the Software Engineering for Robotics based on the RoboSoft RAEng event is now available.
17/02/21: Our grant proposal on Verifiably Correct Swarm Attestation will be funded! (Value: £514k)
03/02/21: Our paper Verifying Correctness of Persistent Concurrent Data Structures: A Sound and Complete Method was accepted for publication in Formal Aspects of Computing.
13/01/21: Our paper Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras was accepted for publication in LMCS. Preprint