Brijesh Dongol

According to our database, Brijesh Dongol authored at least 100 papers between 2005 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

A Fully Verified Persistency Library.

Stefan Bodenmüller, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2024

Artifact Report: Intel PMDK Transactions: Specification, Validation and Concurrency.

Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol

Proceedings of the Programming Languages and Systems, 2024

Intel PMDK Transactions: Specification, Validation and Concurrency.

Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol

Proceedings of the Programming Languages and Systems, 2024

2023

Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies.

Daniel Wright, Sadegh Dalvandi, Mark Batty, Brijesh Dongol

Formal Aspects Comput., June, 2023

Intel PMDK Transactions: Specification, Validation and Concurrency (Extended Version).

Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol

CoRR, 2023

Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version).

Ori Lahav, Brijesh Dongol, Heike Wehrheim

CoRR, 2023

Verifying List Swarm Attestation Protocols.

Jay Le-Papin, Brijesh Dongol, Helen Treharne, Stephan Wesemeyer

Proceedings of the 16th ACM Conference on Security and Privacy in Wireless and Mobile Networks, 2023

Verifying Read-Copy Update Under RC11.

Mikhail Semenyuk, Mark Batty, Brijesh Dongol

Proceedings of the Software Engineering and Formal Methods - 21st International Conference, 2023

Ownership-Based Owicki-Gries Reasoning.

Mikhail Semenyuk, Brijesh Dongol

Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing, 2023

Reasoning About Promises in Weak Memory Models with Event Structures.

Heike Wehrheim, Lara Bargmann, Brijesh Dongol

Proceedings of the Formal Methods - 25th International Symposium, 2023

Rely-Guarantee Reasoning for Causally Consistent Shared Memory.

Ori Lahav, Brijesh Dongol, Heike Wehrheim

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2022

Unifying Operational Weak Memory Verification: An Axiomatic Approach.

Simon Doherty, Sadegh Dalvandi, Brijesh Dongol, Heike Wehrheim

ACM Trans. Comput. Log., 2022

Implementing and verifying release-acquire transactional memory in C11.

Sadegh Dalvandi, Brijesh Dongol

Proc. ACM Program. Lang., 2022

Modularising Verification Of Durable Opacity.

Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim

Log. Methods Comput. Sci., 2022

Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL.

Sadegh Dalvandi, Brijesh Dongol, Simon Doherty, Heike Wehrheim

J. Autom. Reason., 2022

A blockchain-enabled e-learning platform.

Tsz Yiu Lam, Brijesh Dongol

Interact. Learn. Environ., 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

Formal Aspects Comput., 2022

Introduction to the Special Section on iFM 2020.

Brijesh Dongol, Elena Troubitsyna

Formal Aspects Comput., 2022

Reasoning about Promises in Weak Memory Models with Event Structures (Extended Version).

Heike Wehrheim, Lara Bargmann, Brijesh Dongol

CoRR, 2022

Implementing and Verifying Release-Acquire Transactional Memory (Extended Version).

Sadegh Dalvandi, Brijesh Dongol

CoRR, 2022

View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version).

Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson

CoRR, 2022

Proving Memory Access Violations in Isabelle/HOL.

Sharar Ahmadi, Brijesh Dongol, Matt Griffin

Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems, 2022

View-Based Owicki-Gries Reasoning for Persistent x86-TSO.

Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson

Proceedings of the Programming Languages and Systems, 2022

Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement.

Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim

Proceedings of the 33rd International Conference on Concurrency Theory, 2022

2021

Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras.

Brijesh Dongol, Ian J. Hayes, Georg Struth

Log. Methods Comput. Sci., 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

Verifying C11-Style Weak Memory Libraries via Refinement.

Sadegh Dalvandi, Brijesh Dongol

CoRR, 2021

Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version).

Daniel Wright, Mark Batty, Brijesh Dongol

CoRR, 2021

On Strong Observational Refinement and Forward Simulation.

John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim

CoRR, 2021

Brief Announcement: On Strong Observational Refinement and Forward Simulation.

John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim

Proceedings of the 35th International Symposium on Distributed Computing, 2021

Checking Opacity and Durable Opacity with FDR.

Brijesh Dongol, Jay Le-Papin

Proceedings of the Software Engineering and Formal Methods - 19th International Conference, 2021

Verifying C11-style weak memory libraries.

Sadegh Dalvandi, Brijesh Dongol

Proceedings of the PPoPP '21: 26th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2021

Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies.

Daniel Wright, Mark Batty, Brijesh Dongol

Proceedings of the Formal Methods - 24th International Symposium, 2021

Verifying Secure Speculation in Isabelle/HOL.

Matt Griffin, Brijesh Dongol

Proceedings of the Formal Methods - 24th International Symposium, 2021

2020

Owicki-Gries Reasoning for C11 RAR (Artifact).

Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, Heike Wehrheim

Dagstuhl Artifacts Ser., 2020

Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL.

Sadegh Dalvandi, Brijesh Dongol, Simon Doherty

CoRR, 2020

Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory.

Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2020

Owicki-Gries Reasoning for C11 RAR.

Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, Heike Wehrheim

Proceedings of the 34th European Conference on Object-Oriented Programming, 2020

2019

Modular transactions: bounding mixed races in space and time.

Brijesh Dongol, Radha Jagadeesan, James Riely

Proceedings of the 24th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2019

Verifying C11 programs operationally.

Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick

Proceedings of the 24th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2019

Cylindric Kleene Lattices for Program Construction.

Brijesh Dongol, Ian J. Hayes, Larissa Meinicke, Georg Struth

Proceedings of the Mathematics of Program Construction - 13th International Conference, 2019

Verifying Correctness of Persistent Concurrent Data Structures.

John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim

Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs.

Keith Clark, Brijesh Dongol, Peter Robinson

Proceedings of the Formal Methods. FM 2019 International Workshops, 2019

Towards deductive verification of C11 programs with Event-B and ProB.

Mohammadsadegh Dalvandi, Brijesh Dongol

Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, 2019

2018

Transactions in relaxed memory architectures.

Brijesh Dongol, Radha Jagadeesan, James Riely

Proc. ACM Program. Lang., 2018

Mechanized proofs of opacity: a comparison of two techniques.

John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim

Formal Aspects Comput., 2018

Causal Linearizability: Compositionality for Partially Ordered Executions.

Simon Doherty, John Derrick, Brijesh Dongol, Heike Wehrheim

CoRR, 2018

Brief Announcement: Generalising Concurrent Correctness to Weak Memory.

Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick

Proceedings of the 32nd International Symposium on Distributed Computing, 2018

On abstraction and compositionality for weak-memory linearisability.

Brijesh Dongol, Radha Jagadeesan, James Riely, Alasdair Armstrong

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2018

Making Linearizability Compositional for Partially Ordered Executions.

Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick

Proceedings of the Integrated Formal Methods - 14th International Conference, 2018

2017

Decidability and complexity for quiescent consistency and its variations.

Brijesh Dongol, Robert M. Hierons

Inf. Comput., 2017

Relational Convolution, Generalised Modalities and Incidence Algebras.

Brijesh Dongol, Ian J. Hayes, Georg Struth

CoRR, 2017

Partial Semigroups and Convolution Algebras.

Brijesh Dongol, Victor B. F. Gomes, Ian J. Hayes, Georg Struth

Arch. Formal Proofs, 2017

Proving Opacity via Linearizability: A Sound and Complete Method.

Alasdair Armstrong, Brijesh Dongol, Simon Doherty

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2017

Modularising Opacity Verification for Hybrid Transactional Memory.

Alasdair Armstrong, Brijesh Dongol

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2017

A Proof Method for Linearizability on TSO Architectures.

John Derrick, Graeme Smith, Lindsay Groves, Brijesh Dongol

Proceedings of the Provably Correct Systems, 2017

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

Reducing Opacity to Linearizability: A Sound and Complete Method.

Alasdair Armstrong, Brijesh Dongol, Simon Doherty

CoRR, 2016

Proving Opacity of a Pessimistic STM.

Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim

Proceedings of the 20th International Conference on Principles of Distributed Systems, 2016

Decidability and Complexity for Quiescent Consistency.

Brijesh Dongol, Robert M. Hierons

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Contextual Trace Refinement for Concurrent Objects: Safety and Progress.

Brijesh Dongol, Lindsay Groves

Proceedings of the Formal Methods and Software Engineering, 2016

An Interval Logic for Stream-Processing Functions: A Convolution-Based Construction.

Brijesh Dongol

Proceedings of the Formal Techniques for Safety-Critical Systems, 2016

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

Verifying Linearisability: A Comparative Survey.

Brijesh Dongol, John Derrick

ACM Comput. Surv., 2015

Towards linking correctness conditions for concurrent objects and contextual trace refinement.

Brijesh Dongol, Lindsay Groves

Proceedings of the Proceedings 17th International Workshop on Refinement, 2015

A Program Construction and Verification Tool for Separation Logic.

Brijesh Dongol, Victor B. F. Gomes, Georg Struth

Proceedings of the Mathematics of Program Construction - 12th International Conference, 2015

Verifying Opacity of a Transactional Mutex Lock.

John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim

Proceedings of the FM 2015: Formal Methods, 2015

Defining Correctness Conditions for Concurrent Objects in Multicore Architectures.

Brijesh Dongol, John Derrick, Lindsay Groves, Graeme Smith

Proceedings of the 29th European Conference on Object-Oriented Programming, 2015

2014

Deriving real-time action systems with multiple time bands using algebraic reasoning.

Brijesh Dongol, Ian J. Hayes, John Derrick

Sci. Comput. Program., 2014

Reasoning about goal-directed real-time teleo-reactive programs.

Brijesh Dongol, Ian J. Hayes, Peter J. Robinson

Formal Aspects Comput., 2014

Convolution, Separation and Concurrency.

Brijesh Dongol, Ian J. Hayes, Georg Struth

CoRR, 2014

Principles for Verification Tools: Separation Logic.

Brijesh Dongol, Victor B. F. Gomes, Georg Struth

CoRR, 2014

Verifying linearizability: A comparative survey.

Brijesh Dongol, John Derrick

CoRR, 2014

Verifying Linearizability on TSO Architectures.

John Derrick, Graeme Smith, Brijesh Dongol

Proceedings of the Integrated Formal Methods - 11th International Conference, 2014

Reasoning Algebraically About Refinement on TSO Architectures.

Brijesh Dongol, John Derrick, Graeme Smith

Proceedings of the Theoretical Aspects of Computing - ICTAC 2014, 2014

Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures.

John Derrick, Graeme Smith, Lindsay Groves, Brijesh Dongol

Proceedings of the Hardware and Software: Verification and Testing, 2014

Quiescent Consistency: Defining and Verifying Relaxed Linearizability.

John Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, Heike Wehrheim

Proceedings of the FM 2014: Formal Methods, 2014

Admit Your Weakness: Verifying Correctness on TSO Architectures.

Graeme Smith, John Derrick, Brijesh Dongol

Proceedings of the Formal Aspects of Component Software - 11th International Symposium, 2014

2013

Deriving real-time action systems in a sampling logic.

Brijesh Dongol, Ian J. Hayes

Sci. Comput. Program., 2013

Simplifying proofs of linearisability using layers of abstraction.

Brijesh Dongol, John Derrick

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013

Data refinement for true concurrency

Brijesh Dongol, John Derrick

Proceedings of the Proceedings 16th International Refinement Workshop, 2013

Comparing Degrees of Non-Determinism in Expression Evaluation.

Ian J. Hayes, Alan Burns, Brijesh Dongol, Cliff B. Jones

Comput. J., 2013

A High-Level Semantics for Program Execution under Total Store Order Memory.

Brijesh Dongol, Oleg Travkin, John Derrick, Heike Wehrheim

Proceedings of the Theoretical Aspects of Computing - ICTAC 2013, 2013

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

Proving linearisability via coarse-grained abstraction

Brijesh Dongol, John Derrick

CoRR, 2012

Deriving Real-Time Action Systems Controllers from Multiscale System Specifications.

Brijesh Dongol, Ian J. Hayes

Proceedings of the Mathematics of Program Construction - 11th International Conference, 2012

Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands.

Brijesh Dongol, Ian J. Hayes

Proceedings of the Integrated Formal Methods - 9th International Conference, 2012

Towards an Algebra for Real-Time Programs.

Brijesh Dongol, Ian J. Hayes, Larissa Meinicke, Kim Solin

Proceedings of the Relational and Algebraic Methods in Computer Science, 2012

2011

Approximating Idealised Real-Time Specifications Using Time Bands.

Brijesh Dongol, Ian J. Hayes

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011

2010

Compositional Action System Derivation Using Enforced Properties.

Brijesh Dongol, Ian J. Hayes

Proceedings of the Mathematics of Program Construction, 10th International Conference, 2010

2009

Progress-based verification and derivation of concurrent programs

Brijesh Dongol

PhD thesis, 2009

A general technique for proving lock-freedom.

Robert Colvin, Brijesh Dongol

Sci. Comput. Program., 2009

Enforcing Safety and Progress Properties: An Approach to Concurrent Program Derivation.

Brijesh Dongol, Ian J. Hayes

Proceedings of the 20th Australian Software Engineering Conference (ASWEC 2009), 2009

2008

Streamlining progress-based derivations of concurrent programs.

Brijesh Dongol, Arjan J. Mooij

Formal Aspects Comput., 2008

2007

Verifying Lock-Freedom Using Well-Founded Orders.

Robert Colvin, Brijesh Dongol

Proceedings of the Theoretical Aspects of Computing, 2007

2006

Extending the theory of Owicki and Gries with a logic of progress.

Brijesh Dongol, Doug Goldson

Log. Methods Comput. Sci., 2006

Progress in Deriving Concurrent Programs: Emphasizing the Role of Stable Guards.

Brijesh Dongol, Arjan J. Mooij

Proceedings of the Mathematics of Program Construction, 8th International Conference, 2006

Formalising Progress Properties of Non-blocking Programs.

Brijesh Dongol

Proceedings of the Formal Methods and Software Engineering, 2006

Derivation of Java Monitors.

Brijesh Dongol

Proceedings of the 17th Australian Software Engineering Conference (ASWEC 2006), 2006

2005

Concurrent Program Design in the Extended Theory of Owicki and Gries.

Doug Goldson, Brijesh Dongol

Proceedings of the Theory of Computing 2005, 2005