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 am very excited to be joining the Formal Methods Europe Teaching committee, promoting teaching and development of formal methods courses. If you are currently teaching a formal methods course, please submit its details to our repository or get in touch with one of the FME Teaching Committee members.
Program committees
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
Cross-Semester: COM3001 (Professional Project)
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
- 2021-2024: PI on EPSRC Cross-RI Grant on Verifiably Correct Swarm Attestation. (Value: £514k).
- 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: £398k)
- 2018-2022. 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.
- Sadegh Dalvandi
- Sharar Ahmadi
PhD students
- Eleni Vafeiadi Bila, confirmed
- Mikhail Semenyuk, confirmed
- Matt Griffin, current
- Jay Le-Papin, current
Alumni
- Mohammad Heydari (now postdoc at Stockholm University)
- Alasdair Armstrong (now postdoc 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
- 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 - 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
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
- 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.
- 06-10/01/20: Presented at the 79th IFIP 2.1 meeting at Otterlo, Netherlands as an observer.
- 26/11/19: I will be on the program committees of ESOP 2021 and TAP 2020.
- 13-14/11/19: Co-organised RoboSoft: software engineering for robotics at the Royal Academy of Engineering.
- 25/09/19: Gave a talk at the Verified Software Workshop on Owicki-Gries reasoning for C11.
- 01/07/19: Faculty matched funding for a PhD on "Persistent systems security and programme verification" was successful.
- 14/06/19: Our paper on "Cylindric Kleene Lattices for Program Construction" has been accepted to MPC 2019.
- 12/06/19: Our paper on "Verifying Correctness of Persistent Concurrent Data Structures" has been accepted to FM 2019.
- 12/06/19: Our paper on "Deductive Verification of C11 Programs with Event-B and ProB" has been accepted to FTfJP 2019.
- 31/05/19: Funding for our project "FaCT: Faithful Composition of Trust" was successful.
- 01/05/19: Organising the Surrey Concurrency Workshop / S-REPLS (23-24 July).