I am a senior lecturer (associate professor) at the University of Surrey.

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
SBMF 2019, IFM 2019, FMTea 2019 (co-chair), REFINE 2019 (co-chair), MPC 2019, IFM 2018, REFINE 2018 (co-chair), REFINE 2015, PDP 2015.

Semester 1: COM1026 (Foundations of Computing)
Semester 2: COM2022 (Computer Networking), COM3028 (Systems Verification)

  • 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
Post docs

Some previous research and collaborators
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

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

Recent news
  • 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: I am organising the Surrey Concurrency Workshop / S-REPLS (23-24 July).