Brijesh Dongol

I am a 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 a lecturer at Brunel University London from 2014-18 before joining Surrey as a senior lecturer.

Memberships and editorial boards

Program committees
ECOOP 2026, OOPSLA 2026, iFM 2025, ESOP 2025, FMTea 2024, FM 2024 (Tutorial Track), FACS 2024, FACS 2023, FMTea 2023, FACS 2022, iFM 2022, FMTea 2021, CPP 2021, ESOP 2021, IFM 2020 (co-chair), TAP 2020, SBMF 2019, IFM 2019, FMTea 2019 (co-chair), REFINE 2019 (co-chair), MPC 2019, IFM 2018, REFINE 2018 (co-chair), REFINE 2015, PDP 2015.

Teaching
Semester 1: COM1026 (Foundations of Computing)
Semester 2: COM3028 (Systems Verification)

Publications

My list of publications is here. These include links to mechanisation and slides (where available).
My DBLP page is here, and Google Scholar page is here.

Current projects

2024-2027: co-I on CHIST-ERA project REDONDA: A Next-Generation State-Machine Replication Protocol for Blockchain
2023-2027: PI on EPSRC Grant on SACRED-MA: Safe And seCure REmote Direct Memory Access (Value: £1m).
2023-2027: PI on EPSRC Grant on Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT) (Value: £1.5m).
2021-2024: PI on EPSRC Cross-RI Grant on Verifiably Correct Swarm Attestation (Value: £514k).
2018-2024. EPSRC Standard Grant. Co-I on RoboTest: Systematic Model-Based Testing and Simulation of Mobile Autonomous Robots (Value: £610k)
This project fits within the larger RoboCalc umbrella.

Post docs

Daniel Wright

PhD students

Jay Le-Papin, confirmed
Sergey Egorov (co-supervision), confirmed
Sadegh Keshavarzi (co-supervision), confirmed

Alumni

Mikhail Semenyuk (former PhD, now formal verification engineer at Axiomise)
Milad Ketabi
Matt Griffin (former PhD, now postdoc at Imperial College London)
PhD thesis: A Binary Analysis Platform in Isabelle/HOL
Sharar Ahmadi (former PDRA, now research software engineer at the University of Reading)
Eleni Vafeiadi Bila (former PhD, now senior researcher at Arm)
PhD thesis: Specifying and Verifying Persistent Transactional Memory
Sadegh Dalvandi (former PDRA, now formal verification engineer at Axiomise)
Mohammad Heydari (former PDRA, now postdoc at Stockholm University)
Alasdair Armstrong (former PDRA, now researcher with Peter Sewell in Cambridge)

Some previous research and collaborators

Proofs of linearisability with John Derrick, Gerhard Schellhorn, and Heike Wehrheim (2012-14, University of Sheffield)
Time bands and sampling logics for teleo-reactive programs with Ian Hayes (2009-12, University of Queensland)
Progress properties of non-blocking algorithms with Rob Colvin
Concurrent program derivations with Arjan Mooij

Completed projects

2019-2022. VeTSS PhD studentship. PI on Persistent Safety and Security (Value: £78k VeTSS + £78k DCSA matched funding)
2019-2021. ARC Discovery Grant. Co-I on Design and verification of correct, efficient and secure concurrent systems (Value: AU$ 450k)
2018-2020. EPSRC Standard Grant. PI on Verifiably correct transactional memory (Value: £1.1m)
2020: PI on VeTSS small grant on Transactional Security. (Value: £30k).
2019-2021. PI on FaCT: Faithful Composition of Trust. (Value: £204k)
2017-2019. EPSRC Overseas Travel Grant. PI on Verifiably correct concurrency abstractions (Value: £14k)
2016-17. EPSRC First Grant (PI)
Verifiably correct high-performance concurrency libraries for multi-core computing systems (Value: £125k)
2015-16. Brunel University (PI)
Verifying energy-aware networks on chip systems
2015-16. Brunel University New Staff Grant (PI)
2012. University of Sheffield SEED Grant (PI)
Verifiable real-time controllers with multi-timescale requirements
2009. University of Queensland New Staff Research Start-Up Fund
A logic for reasoning about progress properties of teleo-reactive programs
2009. The University of Queensland ResTeach Award

Events organised

Formal Specification and Validation at Scale at the Isaac Newton Institute (2024)
RoboSoft: software engineering for robotics at the Royal Academy of Engineering (2019)
Surrey Concurrency Workshop / S-REPLS (23-24 July, 2019)

Contact details

E-mail: b.dongol [[at]] surrey [[dot]] ac [[dot]] uk

Office: 13BB03

Mailing address:
Department of Computer Science
University of Surrey
Guildford, GU2 7JP
UNITED KINGDOM

Recent news

30/06/25: Our Dagstuhl Seminar Proposal: Foundations of Disaggregated Memory and Heterogeneous Architectures has been accepted
26/05/25: Paper accepted to the ApPLIED Workshop at PODC: Fast Durably Linearizable Data Structures for Free
21/04/25: Paper accepted to ECOOP: IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL
28/01/25: Paper to appear in the Festschrift in honour of Wolfgang Reif: Mirror is Not Strong: Discovery of a Persistent Memory Bug using Refinement in KIV

2024

25/10/24: Paper accepted to ACM InRoads: CS2023: The Role of Formal Methods in Computer Science Education
21/10/24: Co-organised the Formal Specification and Validation at Scale Event at the Isaac Newton Institute.
24/07/24: Paper accepted to DISC: What Cannot Be Implemented on Weak Memory? Preprint
19/07/24: Paper accepted to FMSD Journal: A Verified Durable Transactional Mutex Lock for Persistent x86-TSO
22/06/24: Paper accepted to OOPSLA: Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures
10/06/24: Paper accepted to FM: Unifying Weak Memory Verification using Potentials
20/05/24: Paper accepted to Formal Aspects of Computing journal: On Formal Methods Thinking in Computer Science Education
1/05/24: Paper accepted to USENIX ATC: Mangosteen: Fast Transparent Durability for Linearizable Applications using NVM
23/01/24: Paper accepted to the Science of Computer Programming journal: Operationally Proving Memory Access Violations in Isabelle/HOL
18/01/24: Paper accepted to CSF 2024: Relative Security: Formally Modeling and (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities.
15/01/24: Co-organised the Future of Weak Memory Workshop

2023

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

Archived news