Brijesh Dongol

ORCID

Publication Activity (10 Years)

Years Active: 2005-2024
Publications (10 Years): 72

Top Venues

CoRR

Formal Aspects Comput.

FORTE

Publications

Armando Castañeda, Gregory V. Chockler, Brijesh Dongol, Ori Lahav
What Cannot Be Implemented on Weak Memory? CoRR (2024)
Stefan Bodenmüller, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
A Fully Verified Persistency Library. VMCAI (2) (2024)
Brijesh Dongol, Matthew Griffin, Andrei Popescu, Jamie Wright
Secret-Directed Unwinding. Arch. Formal Proofs 2024 (2024)
Sharar Ahmadi, Brijesh Dongol, Matt Griffin
Operationally proving memory access violations in Isabelle/HOL. Sci. Comput. Program. 234 (2024)
Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol
Intel PMDK Transactions: Specification, Validation and Concurrency. ESOP (2) (2024)
Sharar Ahmadi, Jay Le-Papin, Liqun Chen, Brijesh Dongol, Sasa Radomirovic, Helen Treharne
On the Design and Security of Collective Remote Attestation Protocols. CoRR (2024)
Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol
Artifact Report: Intel PMDK Transactions: Specification, Validation and Concurrency. ESOP (2) (2024)
Sergey Egorov, Gregory V. Chockler, Brijesh Dongol, Dan O'Keeffe, Sadegh Keshavarzi
Mangosteen: Fast Transparent Durability for Linearizable Applications using NVM. USENIX ATC (2024)
Jay Le-Papin, Brijesh Dongol, Helen Treharne, Stephan Wesemeyer
Verifying List Swarm Attestation Protocols. WISEC (2023)
Ori Lahav, Brijesh Dongol, Heike Wehrheim
Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version). CoRR (2023)
Heike Wehrheim, Lara Bargmann, Brijesh Dongol
Reasoning About Promises in Weak Memory Models with Event Structures. FM (2023)
Mikhail Semenyuk, Mark Batty, Brijesh Dongol
Verifying Read-Copy Update Under RC11. SEFM (2023)
Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol
Intel PMDK Transactions: Specification, Validation and Concurrency (Extended Version). CoRR (2023)
Daniel Wright, Sadegh Dalvandi, Mark Batty, Brijesh Dongol
Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies. Formal Aspects Comput. 35 (2) (2023)
Mikhail Semenyuk, Brijesh Dongol
Ownership-Based Owicki-Gries Reasoning. SAC (2023)
Ori Lahav, Brijesh Dongol, Heike Wehrheim
Rely-Guarantee Reasoning for Causally Consistent Shared Memory. CAV (1) (2023)
Simon Doherty, Sadegh Dalvandi, Brijesh Dongol, Heike Wehrheim
Unifying Operational Weak Memory Verification: An Axiomatic Approach. ACM Trans. Comput. Log. 23 (4) (2022)
Tsz Yiu Lam, Brijesh Dongol
A blockchain-enabled e-learning platform. Interact. Learn. Environ. 30 (7) (2022)
Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement. CONCUR (2022)
Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson
View-Based Owicki-Gries Reasoning for Persistent x86-TSO. ESOP (2022)
Sadegh Dalvandi, Brijesh Dongol
Implementing and Verifying Release-Acquire Transactional Memory (Extended Version). CoRR (2022)
Brijesh Dongol, Elena Troubitsyna
Introduction to the Special Section on iFM 2020. Formal Aspects Comput. 34 (1) (2022)
Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson
View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version). CoRR (2022)
Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
Modularising Verification Of Durable Opacity. Log. Methods Comput. Sci. 18 (3) (2022)
Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter W. V. Tran-Jørgensen, James Woodcock
A Survey of Practical Formal Methods for Security. Formal Aspects Comput. 34 (1) (2022)
Heike Wehrheim, Lara Bargmann, Brijesh Dongol
Reasoning about Promises in Weak Memory Models with Event Structures (Extended Version). CoRR (2022)
Sharar Ahmadi, Brijesh Dongol, Matt Griffin
Proving Memory Access Violations in Isabelle/HOL. FTSCS (2022)
Sadegh Dalvandi, Brijesh Dongol
Implementing and verifying release-acquire transactional memory in C11. Proc. ACM Program. Lang. 6 (OOPSLA2) (2022)
Sadegh Dalvandi, Brijesh Dongol, Simon Doherty, Heike Wehrheim
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. J. Autom. Reason. 66 (1) (2022)
John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
Verifying correctness of persistent concurrent data structures: a sound and complete method. Formal Aspects Comput. 33 (4-5) (2021)
John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
Brief Announcement: On Strong Observational Refinement and Forward Simulation. DISC (2021)
Daniel Wright, Mark Batty, Brijesh Dongol
Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version). CoRR (2021)
Matt Griffin, Brijesh Dongol
Verifying Secure Speculation in Isabelle/HOL. FM (2021)
Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter Würtz Vinther Tran-Jørgensen, Jim Woodcock
A Survey of Practical Formal Methods for Security. CoRR (2021)
Sadegh Dalvandi, Brijesh Dongol
Verifying C11-Style Weak Memory Libraries via Refinement. CoRR (2021)
Brijesh Dongol, Ian J. Hayes, Georg Struth
Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras. Log. Methods Comput. Sci. 17 (1) (2021)
Sadegh Dalvandi, Brijesh Dongol
Verifying C11-style weak memory libraries. PPoPP (2021)
Brijesh Dongol, Jay Le-Papin
Checking Opacity and Durable Opacity with FDR. SEFM (2021)
Daniel Wright, Mark Batty, Brijesh Dongol
Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies. FM (2021)
John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
On Strong Observational Refinement and Forward Simulation. CoRR (2021)
Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim
Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. CoRR (2020)
Sadegh Dalvandi, Brijesh Dongol, Simon Doherty
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. CoRR (2020)
Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim
Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. FORTE (2020)
Sadegh Dalvandi, Brijesh Dongol
Verifying C11-Style Weak Memory Libraries. CoRR (2020)
Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, Heike Wehrheim
Owicki-Gries Reasoning for C11 RAR. ECOOP (2020)
Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
Modularising Verification Of Durable Opacity. CoRR (2020)
Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, Heike Wehrheim
Owicki-Gries Reasoning for C11 RAR (Artifact). Dagstuhl Artifacts Ser. 6 (2) (2020)
Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick
Verifying C11 programs operationally. PPoPP (2019)
Keith Clark, Brijesh Dongol, Peter Robinson
Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs. FM Workshops (1) (2019)
Brijesh Dongol, Radha Jagadeesan, James Riely
Modular transactions: bounding mixed races in space and time. PPoPP (2019)
Mohammadsadegh Dalvandi, Brijesh Dongol
Towards deductive verification of C11 programs with Event-B and ProB. FTfJP@ECOOP (2019)
Brijesh Dongol, Ian J. Hayes, Larissa Meinicke, Georg Struth
Cylindric Kleene Lattices for Program Construction. MPC (2019)
John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
Verifying Correctness of Persistent Concurrent Data Structures. FM (2019)
Brijesh Dongol, Radha Jagadeesan, James Riely
Transactions in relaxed memory architectures. Proc. ACM Program. Lang. 2 (POPL) (2018)
Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick
Verifying C11 Programs Operationally. CoRR (2018)
Brijesh Dongol, Radha Jagadeesan, James Riely, Alasdair Armstrong
On abstraction and compositionality for weak-memory linearisability. VMCAI (2018)
John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
Mechanized proofs of opacity: a comparison of two techniques. Formal Aspects Comput. 30 (5) (2018)
Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick
Brief Announcement: Generalising Concurrent Correctness to Weak Memory. DISC (2018)
Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick
Making Linearizability Compositional for Partially Ordered Executions. IFM (2018)
Simon Doherty, John Derrick, Brijesh Dongol, Heike Wehrheim
Causal Linearizability: Compositionality for Partially Ordered Executions. CoRR (2018)
Brijesh Dongol, Robert M. Hierons
Decidability and complexity for quiescent consistency and its variations. Inf. Comput. 257 (2017)
Brijesh Dongol, Ian J. Hayes, Georg Struth
Relational Convolution, Generalised Modalities and Incidence Algebras. CoRR (2017)
Alasdair Armstrong, Brijesh Dongol, Simon Doherty
Proving Opacity via Linearizability: A Sound and Complete Method. FORTE (2017)
Alasdair Armstrong, Brijesh Dongol
Modularising Opacity Verification for Hybrid Transactional Memory. FORTE (2017)
Brijesh Dongol, Victor B. F. Gomes, Ian J. Hayes, Georg Struth
Partial Semigroups and Convolution Algebras. Arch. Formal Proofs 2017 (2017)
Brijesh Dongol
An Interval Logic for Stream-Processing Functions: A Convolution-Based Construction. FTSCS (2016)
Brijesh Dongol, Robert M. Hierons
Decidability and Complexity for Quiescent Consistency. LICS (2016)
Brijesh Dongol, Lindsay Groves
Contextual trace refinement for concurrent objects: Safety and progress. CoRR (2016)
Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim
Proving Opacity of a Pessimistic STM. OPODIS (2016)
Brijesh Dongol, Ian J. Hayes, Georg Struth
Convolution as a Unifying Concept: Applications in Separation Logic, Interval Calculi, and Concurrency. ACM Trans. Comput. Log. 17 (3) (2016)
Brijesh Dongol, Lindsay Groves
Contextual Trace Refinement for Concurrent Objects: Safety and Progress. ICFEM (2016)
Alasdair Armstrong, Brijesh Dongol, Simon Doherty
Reducing Opacity to Linearizability: A Sound and Complete Method. CoRR (2016)
Brijesh Dongol, John Derrick, Lindsay Groves, Graeme Smith
Defining Correctness Conditions for Concurrent Objects in Multicore Architectures. ECOOP (2015)
Brijesh Dongol, John Derrick
Verifying Linearisability: A Comparative Survey. ACM Comput. Surv. 48 (2) (2015)
Brijesh Dongol, John Derrick
Interval-based data refinement: A uniform approach to true concurrency in discrete and real-time systems. Sci. Comput. Program. 111 (2015)
Brijesh Dongol, Lindsay Groves
Towards linking correctness conditions for concurrent objects and contextual trace refinement. Refine@FM (2015)
Brijesh Dongol, Robert M. Hierons
Decidability and Complexity for Quiescent Consistency and its Variations. CoRR (2015)
Brijesh Dongol, Victor B. F. Gomes, Georg Struth
A Program Construction and Verification Tool for Separation Logic. MPC (2015)
John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
Verifying Opacity of a Transactional Mutex Lock. FM (2015)
John Derrick, Graeme Smith, Lindsay Groves, Brijesh Dongol
Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures. Haifa Verification Conference (2014)
Brijesh Dongol, John Derrick, Graeme Smith
Reasoning Algebraically About Refinement on TSO Architectures. ICTAC (2014)
John Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, Heike Wehrheim
Quiescent Consistency: Defining and Verifying Relaxed Linearizability. FM (2014)
Brijesh Dongol, Ian J. Hayes, Peter J. Robinson
Reasoning about goal-directed real-time teleo-reactive programs. Formal Aspects Comput. 26 (3) (2014)
Brijesh Dongol, Victor B. F. Gomes, Georg Struth
Principles for Verification Tools: Separation Logic. CoRR (2014)
Brijesh Dongol, Ian J. Hayes, Georg Struth
Convolution, Separation and Concurrency. CoRR (2014)
Brijesh Dongol, Ian J. Hayes, John Derrick
Deriving real-time action systems with multiple time bands using algebraic reasoning. Sci. Comput. Program. 85 (2014)
Brijesh Dongol, John Derrick
Verifying linearizability: A comparative survey. CoRR (2014)
Graeme Smith, John Derrick, Brijesh Dongol
Admit Your Weakness: Verifying Correctness on TSO Architectures. FACS (2014)
John Derrick, Graeme Smith, Brijesh Dongol
Verifying Linearizability on TSO Architectures. IFM (2014)
Brijesh Dongol, Oleg Travkin, John Derrick, Heike Wehrheim
A High-Level Semantics for Program Execution under Total Store Order Memory. ICTAC (2013)
Brijesh Dongol, John Derrick
Data refinement for true concurrency Refine@IFM (2013)
Ian J. Hayes, Alan Burns, Brijesh Dongol, Cliff B. Jones
Comparing Degrees of Non-Determinism in Expression Evaluation. Comput. J. 56 (6) (2013)
Brijesh Dongol, Ian J. Hayes
Deriving real-time action systems in a sampling logic. Sci. Comput. Program. 78 (11) (2013)
Brijesh Dongol, John Derrick
Simplifying proofs of linearisability using layers of abstraction. CoRR (2013)
Brijesh Dongol, John Derrick
Simplifying proofs of linearisability using layers of abstraction. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 66 (2013)
Brijesh Dongol, Ian J. Hayes
Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands. IFM (2012)
Brijesh Dongol, John Derrick, Ian J. Hayes
Fractional Permissions and Non-Deterministic Evaluators in Interval Temporal Logic. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 53 (2012)
Brijesh Dongol, Ian J. Hayes, Larissa Meinicke, Kim Solin
Towards an Algebra for Real-Time Programs. RAMiCS (2012)
Brijesh Dongol, Ian J. Hayes
Deriving Real-Time Action Systems Controllers from Multiscale System Specifications. MPC (2012)
Brijesh Dongol, John Derrick
Proving linearisability via coarse-grained abstraction CoRR (2012)

Brijesh Dongol.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Brijesh Dongol