I am a
Reader at the University of Surrey and co-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
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.
Memberships and Editorial Boards
Formal Methods Europe Teaching committee, Formal Aspects of Computing Editorial Board, ACM CS202X panel on Programming Languages
iFM 2022, FMTea 2021, CPP 2021, ESOP 2021, IFM 2020 (co-chair), TAP 2020,
FMTea 2019 (co-chair),
COM1026 (Foundations of Computing)
COM3028 (Systems Verification)
My list of publications is here. These
include links to mechanisation and slides (where available).
My DBLP page
here, and Google Scholar page
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
(Value: £514k). Verifiably Correct Swarm Attestation. 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-2022. EPSRC Standard Grant. Co-I on
(Value: £610k) RoboTest: Systematic Model-Based Testing and Simulation of
Mobile Autonomous Robots
This project fits within the larger RoboCalc umbrella.
Eleni Vafeiadi Bila, confirmed
Mikhail Semenyuk, confirmed
Matt Griffin, confirmed
Jay Le-Papin, confirmed
Some previous research and collaborators
2018-2020. EPSRC Standard Grant. PI on
(Value: £1.1m) Verifiably correct transactional memory 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
2016-17. EPSRC First Grant (PI)
Verifiably correct high-performance concurrency
libraries for multi-core computing systems
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
2009. University of Queensland New Staff Research Start-Up
for reasoning about progress properties of teleo-reactive
2009. The University of Queensland ResTeach Award
Here is a talk on our paper Transactions in Relaxed Memory Architectures given by James Riely at POPL 2018.
Here is a talk on our paper Defining correctness conditions for concurrent objects in multicore architectures I gave at ECOOP 2015.
E-mail: b.dongol [[at]] surrey [[dot]] ac [[dot]] uk
You can find me in 07BB02
Department of Computer Science
University of Surrey
Guildford, GU2 7JP
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".
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.
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
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
16/11/20: Our paper "Verifying C11-Style Weak Memory Libraries" was accepted as a poster at PPoPP 2021. Full paper.
14/05/20: Our paper "Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory" was awarded best paper at FORTE 2020!
10/04/20: Our paper "Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory" was accepted to FORTE 2020.
preprint 9/04/20: Our paper "Owicki-Gries Reasoning for C11 RAR" was accepted to ECOOP 2020.
preprint 04/02/20: Received a VeTSS small grant to start in April, 2020.
21/01/20: Elena Troubitsyna and I will be PC chairs for