| 2026 | ESOP | Specifying and Verifying RDMA Synchronisation. | Guillaume Ambal, Max Stupple, Brijesh Dongol, Azalea Raad |
| 2026 | FM | Reasoning over Relaxed Shared Memory Models: A Tutorial. | Brijesh Dongol |
| 2025 | ECOOP | IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL. | Matt Griffin, Brijesh Dongol, Azalea Raad |
| 2025 | IFM | Model Checking Buffered Durable Linearizability in CSP. | Chelsea Edmonds, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim |
| 2024 | ESOP | Intel PMDK Transactions: Specification, Validation and Concurrency. | Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol |
| 2024 | ESOP | Artifact Report: Intel PMDK Transactions: Specification, Validation and Concurrency. | Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol |
| 2024 | FM | Unifying Weak Memory Verification Using Potentials. | Lara Bargmann, Brijesh Dongol, Heike Wehrheim |
| 2024 | USENIX | Mangosteen: Fast Transparent Durability for Linearizable Applications using NVM. | Sergey Egorov, Gregory V. Chockler, Brijesh Dongol, Dan O'Keeffe, Sadegh Keshavarzi |
| 2024 | VMCAI | A Fully Verified Persistency Library. | Stefan Bodenmller, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim |
| 2023 | CAV | Rely-Guarantee Reasoning for Causally Consistent Shared Memory. | Ori Lahav, Brijesh Dongol, Heike Wehrheim |
| 2023 | FM | Reasoning About Promises in Weak Memory Models with Event Structures. | Heike Wehrheim, Lara Bargmann, Brijesh Dongol |
| 2023 | SAC | Ownership-Based Owicki-Gries Reasoning. | Mikhail Semenyuk, Brijesh Dongol |
| 2023 | SEFM | Verifying Read-Copy Update Under RC11. | Mikhail Semenyuk, Mark Batty, Brijesh Dongol |
| 2022 | CONCUR | Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement. | Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim |
| 2022 | ESOP | View-Based Owicki-Gries Reasoning for Persistent x86-TSO. | Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson |
| 2021 | FM | Verifying Secure Speculation in Isabelle/HOL. | Matt Griffin, Brijesh Dongol |
| 2021 | FM | Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies. | Daniel Wright, Mark Batty, Brijesh Dongol |
| 2021 | PPoPP | Verifying C11-style weak memory libraries. | Sadegh Dalvandi, Brijesh Dongol |
| 2021 | SEFM | Checking Opacity and Durable Opacity with FDR. | Brijesh Dongol, Jay Le-Papin |
| 2020 | ECOOP | Owicki-Gries Reasoning for C11 RAR. | Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, Heike Wehrheim |
| 2020 | FORTE | Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. | Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim |
| 2019 | ECOOP | Towards deductive verification of C11 programs with Event-B and ProB. | Mohammadsadegh Dalvandi, Brijesh Dongol |
| 2019 | FM | Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs. | Keith Clark, Brijesh Dongol, Peter Robinson |
| 2019 | FM | Verifying Correctness of Persistent Concurrent Data Structures. | John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim |
| 2019 | MPC | Cylindric Kleene Lattices for Program Construction. | Brijesh Dongol, Ian J. Hayes, Larissa Meinicke, Georg Struth |
| 2019 | PPoPP | Verifying C11 programs operationally. | Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick |
| 2019 | PPoPP | Modular transactions: bounding mixed races in space and time. | Brijesh Dongol, Radha Jagadeesan, James Riely |
| 2018 | IFM | Making Linearizability Compositional for Partially Ordered Executions. | Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick |
| 2018 | VMCAI | On abstraction and compositionality for weak-memory linearisability. | Brijesh Dongol, Radha Jagadeesan, James Riely, Alasdair Armstrong |
| 2017 | FORTE | Modularising Opacity Verification for Hybrid Transactional Memory. | Alasdair Armstrong, Brijesh Dongol |
| 2017 | FORTE | Proving Opacity via Linearizability: A Sound and Complete Method. | Alasdair Armstrong, Brijesh Dongol, Simon Doherty |
| 2016 | ICFEM | Contextual Trace Refinement for Concurrent Objects: Safety and Progress. | Brijesh Dongol, Lindsay Groves |
| 2016 | LICS | Decidability and Complexity for Quiescent Consistency. | Brijesh Dongol, Robert M. Hierons |
| 2016 | OPODIS | Proving Opacity of a Pessimistic STM. | Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim |
| 2015 | ECOOP | Defining Correctness Conditions for Concurrent Objects in Multicore Architectures. | Brijesh Dongol, John Derrick, Lindsay Groves, Graeme Smith |
| 2015 | FM | Verifying Opacity of a Transactional Mutex Lock. | John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim |
| 2015 | MPC | A Program Construction and Verification Tool for Separation Logic. | Brijesh Dongol, Victor B. F. Gomes, Georg Struth |
| 2014 | FM | Quiescent Consistency: Defining and Verifying Relaxed Linearizability. | John Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, Heike Wehrheim |
| 2014 | ICTAC | Reasoning Algebraically About Refinement on TSO Architectures. | Brijesh Dongol, John Derrick, Graeme Smith |
| 2014 | IFM | Verifying Linearizability on TSO Architectures. | John Derrick, Graeme Smith, Brijesh Dongol |
| 2013 | ICTAC | A High-Level Semantics for Program Execution under Total Store Order Memory. | Brijesh Dongol, Oleg Travkin, John Derrick, Heike Wehrheim |
| 2012 | IFM | Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands. | Brijesh Dongol, Ian J. Hayes |
| 2012 | MPC | Deriving Real-Time Action Systems Controllers from Multiscale System Specifications. | Brijesh Dongol, Ian J. Hayes |
| 2010 | MPC | Compositional Action System Derivation Using Enforced Properties. | Brijesh Dongol, Ian J. Hayes |
| 2007 | ICTAC | Verifying Lock-Freedom Using Well-Founded Orders. | Robert Colvin, Brijesh Dongol |
| 2006 | ICFEM | Formalising Progress Properties of Non-blocking Programs. | Brijesh Dongol |
| 2006 | MPC | Progress in Deriving Concurrent Programs: Emphasizing the Role of Stable Guards. | Brijesh Dongol, Arjan J. Mooij |