Concurrent Program Design in the Extended Theory of Owicki and Gries. - Doug Goldson; Brijesh Dongol (CATS, 2005)

Derivation of Java Monitors. - Brijesh Dongol (ASWEC, 2006)

Formalising Progress Properties of Non-blocking Programs. - Brijesh Dongol (ICFEM, 2006)

Progress in Deriving Concurrent Programs: Emphasizing the Role of Stable Guards. - Brijesh Dongol; Arjan J. Mooij (MPC, 2006)

Extending the theory of Owicki and Gries with a logic of progress. - Brijesh Dongol; Doug Goldson (Log. Methods Comput. Sci., 2006)

Verifying Lock-Freedom Using Well-Founded Orders. - Robert Colvin; Brijesh Dongol (ICTAC, 2007)

Streamlining progress-based derivations of concurrent programs. - Brijesh Dongol; Arjan J. Mooij (Formal Aspects Comput., 2008)

Enforcing Safety and Progress Properties: An Approach to Concurrent Program Derivation. - Brijesh Dongol; Ian J. Hayes (Australian Software Engineering Conference, 2009)

A general technique for proving lock-freedom. - Robert Colvin; Brijesh Dongol (Sci. Comput. Program., 2009)

Progress-based verification and derivation of concurrent programs - Brijesh Dongol (2009)

Compositional Action System Derivation Using Enforced Properties. - Brijesh Dongol; Ian J. Hayes (MPC, 2010)

Approximating Idealised Real-Time Specifications Using Time Bands. - Brijesh Dongol; Ian J. Hayes (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011)

Towards an Algebra for Real-Time Programs. - Brijesh Dongol; Ian J. Hayes; Larissa Meinicke; Kim Solin (RAMiCS, 2012)

Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands. - Brijesh Dongol; Ian J. Hayes (IFM, 2012)

Deriving Real-Time Action Systems Controllers from Multiscale System Specifications. - Brijesh Dongol; Ian J. Hayes (MPC, 2012)

Proving linearisability via coarse-grained abstraction - Brijesh Dongol; John Derrick (CoRR, 2012)

Fractional Permissions and Non-Deterministic Evaluators in Interval Temporal Logic. - Brijesh Dongol; John Derrick; Ian J. Hayes (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012)

A High-Level Semantics for Program Execution under Total Store Order Memory. - Brijesh Dongol; Oleg Travkin 001; John Derrick; Heike Wehrheim (ICTAC, 2013)

Comparing Degrees of Non-Determinism in Expression Evaluation. - Ian J. Hayes; Alan Burns 001; Brijesh Dongol; Cliff B. Jones (Comput. J., 2013)

Data refinement for true concurrency - Brijesh Dongol; John Derrick (Refine@IFM, 2013)

Simplifying proofs of linearisability using layers of abstraction. - Brijesh Dongol; John Derrick (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

Deriving real-time action systems in a sampling logic. - Brijesh Dongol; Ian J. Hayes (Sci. Comput. Program., 2013)

Admit Your Weakness: Verifying Correctness on TSO Architectures. - Graeme Smith 001; John Derrick; Brijesh Dongol (FACS, 2014)

Quiescent Consistency: Defining and Verifying Relaxed Linearizability. - John Derrick; Brijesh Dongol; Gerhard Schellhorn; Bogdan Tofan; Oleg Travkin 001; Heike Wehrheim (FM, 2014)

Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures. - John Derrick; Graeme Smith 001; Lindsay Groves; Brijesh Dongol (Haifa Verification Conference, 2014)

Reasoning Algebraically About Refinement on TSO Architectures. - Brijesh Dongol; John Derrick; Graeme Smith 001 (ICTAC, 2014)

Verifying Linearizability on TSO Architectures. - John Derrick; Graeme Smith 001; Brijesh Dongol (IFM, 2014)

Verifying linearizability: A comparative survey. - Brijesh Dongol; John Derrick (CoRR, 2014)

Principles for Verification Tools: Separation Logic. - Brijesh Dongol; Victor B. F. Gomes; Georg Struth (CoRR, 2014)

Convolution, Separation and Concurrency. - Brijesh Dongol; Ian J. Hayes; Georg Struth (CoRR, 2014)

Reasoning about goal-directed real-time teleo-reactive programs. - Brijesh Dongol; Ian J. Hayes; Peter J. Robinson 001 (Formal Aspects Comput., 2014)

Deriving real-time action systems with multiple time bands using algebraic reasoning. - Brijesh Dongol; Ian J. Hayes; John Derrick (Sci. Comput. Program., 2014)

Defining Correctness Conditions for Concurrent Objects in Multicore Architectures. - Brijesh Dongol; John Derrick; Lindsay Groves; Graeme Smith 001 (ECOOP, 2015)

Verifying Opacity of a Transactional Mutex Lock. - John Derrick; Brijesh Dongol; Gerhard Schellhorn; Oleg Travkin 001; Heike Wehrheim (FM, 2015)

A Program Construction and Verification Tool for Separation Logic. - Brijesh Dongol; Victor B. F. Gomes; Georg Struth (MPC, 2015)

Towards linking correctness conditions for concurrent objects and contextual trace refinement. - Brijesh Dongol; Lindsay Groves (Refine@FM, 2015)

Verifying Linearisability: A Comparative Survey. - Brijesh Dongol; John Derrick (ACM Comput. Surv., 2015)

Interval-based data refinement: A uniform approach to true concurrency in discrete and real-time systems. - Brijesh Dongol; John Derrick (Sci. Comput. Program., 2015)

An Interval Logic for Stream-Processing Functions: A Convolution-Based Construction. - Brijesh Dongol (FTSCS, 2016)

Contextual Trace Refinement for Concurrent Objects: Safety and Progress. - Brijesh Dongol; Lindsay Groves (ICFEM, 2016)

Decidability and Complexity for Quiescent Consistency. - Brijesh Dongol; Robert M. Hierons (LICS, 2016)

Proving Opacity of a Pessimistic STM. - Simon Doherty; Brijesh Dongol; John Derrick; Gerhard Schellhorn; Heike Wehrheim (OPODIS, 2016)

Reducing Opacity to Linearizability: A Sound and Complete Method. - Alasdair Armstrong; Brijesh Dongol; Simon Doherty (CoRR, 2016)

Convolution as a Unifying Concept: Applications in Separation Logic, Interval Calculi, and Concurrency. - Brijesh Dongol; Ian J. Hayes; Georg Struth (ACM Trans. Comput. Log., 2016)

A Proof Method for Linearizability on TSO Architectures. - John Derrick; Graeme Smith 001; Lindsay Groves; Brijesh Dongol (Provably Correct Systems, 2017)

Modularising Opacity Verification for Hybrid Transactional Memory. - Alasdair Armstrong; Brijesh Dongol (FORTE, 2017)

Proving Opacity via Linearizability: A Sound and Complete Method. - Alasdair Armstrong; Brijesh Dongol; Simon Doherty (FORTE, 2017)

Partial Semigroups and Convolution Algebras. - Brijesh Dongol; Victor B. F. Gomes; Ian J. Hayes; Georg Struth (Arch. Formal Proofs, 2017)

Relational Convolution, Generalised Modalities and Incidence Algebras. - Brijesh Dongol; Ian J. Hayes; Georg Struth (CoRR, 2017)

Decidability and complexity for quiescent consistency and its variations. - Brijesh Dongol; Robert M. Hierons (Inf. Comput., 2017)

Making Linearizability Compositional for Partially Ordered Executions. - Simon Doherty; Brijesh Dongol; Heike Wehrheim; John Derrick (IFM, 2018)

On abstraction and compositionality for weak-memory linearisability. - Brijesh Dongol; Radha Jagadeesan; James Riely; Alasdair Armstrong (VMCAI, 2018)

Brief Announcement: Generalising Concurrent Correctness to Weak Memory. - Simon Doherty; Brijesh Dongol; Heike Wehrheim; John Derrick (DISC, 2018)

Causal Linearizability: Compositionality for Partially Ordered Executions. - Simon Doherty; John Derrick; Brijesh Dongol; Heike Wehrheim (CoRR, 2018)

Mechanized proofs of opacity: a comparison of two techniques. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Oleg Travkin 001; Heike Wehrheim (Formal Aspects Comput., 2018)

Transactions in relaxed memory architectures. - Brijesh Dongol; Radha Jagadeesan; James Riely (Proc. ACM Program. Lang., 2018)

Towards deductive verification of C11 programs with Event-B and ProB. - Mohammadsadegh Dalvandi; Brijesh Dongol (FTfJP@ECOOP, 2019)

Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs. - Keith Clark; Brijesh Dongol; Peter Robinson 007 (FM Workshops (1), 2019)

Verifying Correctness of Persistent Concurrent Data Structures. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (FM, 2019)

Cylindric Kleene Lattices for Program Construction. - Brijesh Dongol; Ian J. Hayes; Larissa Meinicke; Georg Struth (MPC, 2019)

Verifying C11 programs operationally. - Simon Doherty; Brijesh Dongol; Heike Wehrheim; John Derrick (PPoPP, 2019)

Modular transactions: bounding mixed races in space and time. - Brijesh Dongol; Radha Jagadeesan; James Riely (PPoPP, 2019)

Owicki-Gries Reasoning for C11 RAR. - Sadegh Dalvandi; Simon Doherty; Brijesh Dongol; Heike Wehrheim (ECOOP, 2020)

Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. - Eleni Bila; Simon Doherty; Brijesh Dongol; John Derrick; Gerhard Schellhorn; Heike Wehrheim (FORTE, 2020)

Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. - Sadegh Dalvandi; Brijesh Dongol; Simon Doherty (CoRR, 2020)

Owicki-Gries Reasoning for C11 RAR (Artifact). - Sadegh Dalvandi; Simon Doherty; Brijesh Dongol; Heike Wehrheim (Dagstuhl Artifacts Ser., 2020)

Verifying Secure Speculation in Isabelle/HOL. - Matt Griffin; Brijesh Dongol (FM, 2021)

Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies. - Daniel Wright 001; Mark Batty; Brijesh Dongol (FM, 2021)

Verifying C11-style weak memory libraries. - Sadegh Dalvandi; Brijesh Dongol (PPoPP, 2021)

Checking Opacity and Durable Opacity with FDR. - Brijesh Dongol; Jay Le-Papin (SEFM, 2021)

Brief Announcement: On Strong Observational Refinement and Forward Simulation. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (DISC, 2021)

On Strong Observational Refinement and Forward Simulation. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (CoRR, 2021)

Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version). - Daniel Wright 001; Mark Batty; Brijesh Dongol (CoRR, 2021)

Verifying C11-Style Weak Memory Libraries via Refinement. - Sadegh Dalvandi; Brijesh Dongol (CoRR, 2021)

Verifying correctness of persistent concurrent data structures: a sound and complete method. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (Formal Aspects Comput., 2021)

Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras. - Brijesh Dongol; Ian J. Hayes; Georg Struth (Log. Methods Comput. Sci., 2021)

Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement. - Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (CONCUR, 2022)

View-Based Owicki-Gries Reasoning for Persistent x86-TSO. - Eleni Vafeiadi Bila; Brijesh Dongol; Ori Lahav 001; Azalea Raad; John Wickerson (ESOP, 2022)

Proving Memory Access Violations in Isabelle/HOL. - Sharar Ahmadi; Brijesh Dongol; Matt Griffin (FTSCS, 2022)

View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version). - Eleni Vafeiadi Bila; Brijesh Dongol; Ori Lahav 001; Azalea Raad; John Wickerson (CoRR, 2022)

Implementing and Verifying Release-Acquire Transactional Memory (Extended Version). - Sadegh Dalvandi; Brijesh Dongol (CoRR, 2022)

Reasoning about Promises in Weak Memory Models with Event Structures (Extended Version). - Heike Wehrheim; Lara Bargmann; Brijesh Dongol (CoRR, 2022)

Introduction to the Special Section on iFM 2020. - Brijesh Dongol; Elena Troubitsyna (Formal Aspects Comput., 2022)

A Survey of Practical Formal Methods for Security. - Tomas Kulik; Brijesh Dongol; Peter Gorm Larsen; Hugo Daniel Macedo; Steve Schneider; Peter W. V. Tran-Jørgensen; Jim Woodcock 001 (Formal Aspects Comput., 2022)

A blockchain-enabled e-learning platform. - Tsz Yiu Lam; Brijesh Dongol (Interact. Learn. Environ., 2022)

Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. - Sadegh Dalvandi; Brijesh Dongol; Simon Doherty; Heike Wehrheim (J. Autom. Reason., 2022)

Modularising Verification Of Durable Opacity. - Eleni Bila; John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (Log. Methods Comput. Sci., 2022)

Implementing and verifying release-acquire transactional memory in C11. - Sadegh Dalvandi; Brijesh Dongol (Proc. ACM Program. Lang., 2022)

Unifying Operational Weak Memory Verification: An Axiomatic Approach. - Simon Doherty; Sadegh Dalvandi; Brijesh Dongol; Heike Wehrheim (ACM Trans. Comput. Log., 2022)

Rely-Guarantee Reasoning for Causally Consistent Shared Memory. - Ori Lahav 001; Brijesh Dongol; Heike Wehrheim (CAV (1), 2023)

Reasoning About Promises in Weak Memory Models with Event Structures. - Heike Wehrheim; Lara Bargmann; Brijesh Dongol (FM, 2023)

Ownership-Based Owicki-Gries Reasoning. - Mikhail Semenyuk; Brijesh Dongol (SAC, 2023)

Verifying Read-Copy Update Under RC11. - Mikhail Semenyuk; Mark Batty; Brijesh Dongol (SEFM, 2023)

Verifying List Swarm Attestation Protocols. - Jay Le-Papin; Brijesh Dongol; Helen Treharne; Stephan Wesemeyer (WISEC, 2023)

Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version). - Ori Lahav 001; Brijesh Dongol; Heike Wehrheim (CoRR, 2023)

Intel PMDK Transactions: Specification, Validation and Concurrency (Extended Version). - Azalea Raad; Ori Lahav 001; John Wickerson; Piotr Balcer; Brijesh Dongol (CoRR, 2023)

Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies. - Daniel Wright 001; Sadegh Dalvandi; Mark Batty; Brijesh Dongol (Formal Aspects Comput., 2023)

Relative Security: Formally Modeling and (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities. - Brijesh Dongol; Matt Griffin; Andrei Popescu 001; Jamie Wright (CSF, 2024)

Intel PMDK Transactions: Specification, Validation and Concurrency. - Azalea Raad; Ori Lahav 001; John Wickerson; Piotr Balcer; Brijesh Dongol (ESOP (2), 2024)

Artifact Report: Intel PMDK Transactions: Specification, Validation and Concurrency. - Azalea Raad; Ori Lahav 001; John Wickerson; Piotr Balcer; Brijesh Dongol (ESOP (2), 2024)

Unifying Weak Memory Verification Using Potentials. - Lara Bargmann; Brijesh Dongol; Heike Wehrheim (FM (1), 2024)

Mangosteen: Fast Transparent Durability for Linearizable Applications using NVM. - Sergey Egorov; Gregory V. Chockler; Brijesh Dongol; Dan O'Keeffe; Sadegh Keshavarzi (USENIX ATC, 2024)

A Fully Verified Persistency Library. - Stefan Bodenmüller; John Derrick; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (VMCAI (2), 2024)

What Cannot Be Implemented on Weak Memory? - Armando Castañeda; Gregory V. Chockler; Brijesh Dongol; Ori Lahav 001 (DISC, 2024)

Secret-Directed Unwinding. - Brijesh Dongol; Matthew Griffin; Andrei Popescu 001; Jamie Wright (Arch. Formal Proofs, 2024)

On the Design and Security of Collective Remote Attestation Protocols. - Sharar Ahmadi; Jay Le-Papin; Liqun Chen 002; Brijesh Dongol; Sasa Radomirovic; Helen Treharne (CoRR, 2024)

Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures. - Guillaume Ambal; Brijesh Dongol; Haggai Eran; Vasileios Klimis; Ori Lahav 001; Azalea Raad (Proc. ACM Program. Lang., 2024)

Operationally proving memory access violations in Isabelle/HOL. - Sharar Ahmadi; Brijesh Dongol; Matt Griffin (Sci. Comput. Program., 2024)

A Rely-Guarantee Framework for Proving Deadlock Freedom Under Causal Consistency. - Brijesh Dongol; Ori Lahav 001; Heike Wehrheim (The Practice of Formal Methods (I), 2024)

A verified durable transactional mutex lock for persistent x86-TSO. - Eleni Vafeiadi Bila; Brijesh Dongol (Formal Methods Syst. Des., 2024)

The Role of Formal Methods in Computer Science Education. - Maurice H. ter Beek; Manfred Broy; Brijesh Dongol (Inroads, 2024)

Mirror is Not Strong: Discovery of a Persistent Memory Bug using Refinement in KIV. - Gerhard Schellhorn; Stefan Bodenmüller; Brijesh Dongol; Heike Wehrheim (Go Where the Bugs Are, 2025)

IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL. - Matt Griffin; Brijesh Dongol; Azalea Raad (ECOOP, 2025)

On Formal Methods Thinking in Computer Science Education. - Brijesh Dongol; Catherine Dubois; Stefan Hallerstede; Eric C. R. Hehner; Carroll Morgan; Peter Müller 001; Leila Ribeiro 001; Alexandra Silva 001; Graeme Smith 001; Erik P. de Vink (Formal Aspects Comput., 2025)

CSP Artifact for Model Checking Buffered Durable Linearizability. - Chelsea Edmonds; Brijesh Dongol; John Derrick; Heike Wehrheim; Gerhard Schellhorn (Zenodo, 2025)

CSP Artifact for Model Checking Buffered Durable Linearizability. - Chelsea Edmonds; Brijesh Dongol; John Derrick; Heike Wehrheim; Gerhard Schellhorn (Zenodo, 2025)

CSP Artifact for Model Checking Buffered Durable Linearizability. - Chelsea Edmonds; Brijesh Dongol; John Derrick; Heike Wehrheim; Gerhard Schellhorn (Zenodo, 2025)

IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL (Extended Version). - Matt Griffin; Brijesh Dongol; Azalea Raad (CoRR, 2025)

CSP Artifact for Model Checking Buffered Durable Linearizability. - Chelsea Edmonds; Brijesh Dongol; John Derrick; Heike Wehrheim; Gerhard Schellhorn (Zenodo, 2025)

CSP Artifact for Model Checking Buffered Durable Linearizability. - Chelsea Edmonds; Brijesh Dongol; John Derrick; Heike Wehrheim; Gerhard Schellhorn (Zenodo, 2025)

A Verified High-Performance Composable Object Library for Remote Direct Memory Access (Extended Version). - Guillaume Ambal; George Hodgkins; Mark Madler; Gregory V. Chockler; Brijesh Dongol; Joseph Izraelevitz; Azalea Raad; Viktor Vafeiadis (CoRR, 2025)