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
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.
Media
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.
Contact details
E-mail: b.dongol [[at]] surrey [[dot]] ac [[dot]] uk
You can find me in 07BB02
Mailing address:
Department of Computer Science
University of Surrey
Guildford, GU2 7JP
UNITED KINGDOM
Recent news
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
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
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 iFM 2020.