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 2019 (co-chair), REFINE 2019 (co-chair), MPC 2019, IFM 2018, REFINE 2018 (co-chair), REFINE 2015, PDP 2015.
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
- 2019-2021. VeTSS studentship (PI)
Persistent Safety and Security NEW! - 2019-2021. ARC Discovery Grant (Co-I)
Design and verification of correct, efficient and secure concurrent systems NEW! - 2018-2020. EPSRC Standard Grant (PI)
Verifiably correct transactional memory - 2018-2022. EPSRC Standard Grant (Co-I)
RoboTest: Systematic Model-Based Testing and Simulation of Mobile Autonomous Robots
This project fits within the larger RoboCalc umbrella. - 2017-2019. EPSRC Overseas Travel Grant (PI)
Verifiably correct concurrency abstractions
- 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
- 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