Brijesh Dongol

136 papers A* 1A 8B 24C 9Misc 1Journal 66Unranked 20

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	A Verified High-Performance Composable Object Library for Remote Direct Memory Access. Proc. ACM Program. Lang. Guillaume Ambal, George Hodgkins, Mark Madler, Gregory V. Chockler, Brijesh Dongol, Joseph Izraelevitz, Azalea Raad, Viktor Vafeiadis
2026	J	`jnl`	Specifying and Verifying RDMA Synchronisation (Extended Version). CoRR Guillaume Ambal, Max Stupple, Brijesh Dongol, Azalea Raad
2026	—	`conf`	Specifying and Verifying RDMA Synchronisation. ESOP (1) Guillaume Ambal, Max Stupple, Brijesh Dongol, Azalea Raad
2025	J	`jnl`	A Verified High-Performance Composable Object Library for Remote Direct Memory Access (Extended Version). CoRR Guillaume Ambal, George Hodgkins, Mark Madler, Gregory V. Chockler, Brijesh Dongol, Joseph Izraelevitz, Azalea Raad, Viktor Vafeiadis
2025	J	`jnl`	IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL (Extended Version). CoRR Matt Griffin, Brijesh Dongol, Azalea Raad
2025	A	`conf`	IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL. ECOOP Matt Griffin, Brijesh Dongol, Azalea Raad
2025	—	`conf`	Mirror is Not Strong: Discovery of a Persistent Memory Bug using Refinement in KIV. Go Where the Bugs Are Gerhard Schellhorn, Stefan Bodenmüller, Brijesh Dongol, Heike Wehrheim
2025	B	`conf`	Model Checking Buffered Durable Linearizability in CSP. iFM Chelsea Edmonds, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2025	J	`jnl`	On Formal Methods Thinking in Computer Science Education. Formal Aspects Comput. Brijesh Dongol, Catherine Dubois, Stefan Hallerstede, Eric C. R. Hehner, Carroll Morgan, Peter Müller, Leila Ribeiro, Alexandra Silva, Graeme Smith, Erik P. de Vink
2025	J	`jnl`	Relative Security: (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities in Isabelle/HOL. J. Autom. Reason. John Derrick, Brijesh Dongol, Chelsea Edmonds, Matt Griffin, Andrei Popescu, Jamie Wright
2024	—	`conf`	A Fully Verified Persistency Library. VMCAI (2) Stefan Bodenmüller, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2024	—	`ch.`	A Rely-Guarantee Framework for Proving Deadlock Freedom Under Causal Consistency. The Practice of Formal Methods (I) Brijesh Dongol, Ori Lahav, Heike Wehrheim
2024	J	`jnl`	A verified durable transactional mutex lock for persistent x86-TSO. Formal Methods Syst. Des. Eleni Vafeiadi Bila, Brijesh Dongol
2024	—	`conf`	Artifact Report: Intel PMDK Transactions: Specification, Validation and Concurrency. ESOP (2) Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol
2024	—	`conf`	Intel PMDK Transactions: Specification, Validation and Concurrency. ESOP (2) Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol
2024	—	`conf`	Mangosteen: Fast Transparent Durability for Linearizable Applications using NVM. USENIX ATC Sergey Egorov, Gregory V. Chockler, Brijesh Dongol, Dan O'Keeffe, Sadegh Keshavarzi
2024	J	`jnl`	On the Design and Security of Collective Remote Attestation Protocols. CoRR Sharar Ahmadi, Jay Le-Papin, Liqun Chen, Brijesh Dongol, Sasa Radomirovic, Helen Treharne
2024	J	`jnl`	Operationally proving memory access violations in Isabelle/HOL. Sci. Comput. Program. Sharar Ahmadi, Brijesh Dongol, Matt Griffin
2024	A	`conf`	Relative Security: Formally Modeling and (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities. CSF Brijesh Dongol, Matt Griffin, Andrei Popescu, Jamie Wright
2024	J	`jnl`	Secret-Directed Unwinding. Arch. Formal Proofs Brijesh Dongol, Matthew Griffin, Andrei Popescu, Jamie Wright
2024	J	`jnl`	Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures. Proc. ACM Program. Lang. Guillaume Ambal, Brijesh Dongol, Haggai Eran, Vasileios Klimis, Ori Lahav, Azalea Raad
2024	J	`jnl`	The Role of Formal Methods in Computer Science Education. Inroads Maurice H. ter Beek, Manfred Broy, Brijesh Dongol
2024	—	`conf`	Unifying Weak Memory Verification Using Potentials. FM (1) Lara Bargmann, Brijesh Dongol, Heike Wehrheim
2024	A	`conf`	What Cannot Be Implemented on Weak Memory? DISC Armando Castañeda, Gregory V. Chockler, Brijesh Dongol, Ori Lahav
2024	J	`jnl`	What Cannot Be Implemented on Weak Memory? CoRR Armando Castañeda, Gregory V. Chockler, Brijesh Dongol, Ori Lahav
2023	J	`jnl`	Intel PMDK Transactions: Specification, Validation and Concurrency (Extended Version). CoRR Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol
2023	J	`jnl`	Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies. Formal Aspects Comput. Daniel Wright, Sadegh Dalvandi, Mark Batty, Brijesh Dongol
2023	Misc	`conf`	Ownership-Based Owicki-Gries Reasoning. SAC Mikhail Semenyuk, Brijesh Dongol
2023	B	`conf`	Reasoning About Promises in Weak Memory Models with Event Structures. FM Heike Wehrheim, Lara Bargmann, Brijesh Dongol
2023	J	`jnl`	Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version). CoRR Ori Lahav, Brijesh Dongol, Heike Wehrheim
2023	—	`conf`	Rely-Guarantee Reasoning for Causally Consistent Shared Memory. CAV (1) Ori Lahav, Brijesh Dongol, Heike Wehrheim
2023	—	`conf`	Verifying List Swarm Attestation Protocols. WISEC Jay Le-Papin, Brijesh Dongol, Helen Treharne, Stephan Wesemeyer
2023	B	`conf`	Verifying Read-Copy Update Under RC11. SEFM Mikhail Semenyuk, Mark Batty, Brijesh Dongol
2022	J	`jnl`	A Survey of Practical Formal Methods for Security. Formal Aspects Comput. Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter W. V. Tran-Jørgensen, Jim Woodcock
2022	J	`jnl`	A blockchain-enabled e-learning platform. Interact. Learn. Environ. Tsz Yiu Lam, Brijesh Dongol
2022	J	`jnl`	Implementing and Verifying Release-Acquire Transactional Memory (Extended Version). CoRR Sadegh Dalvandi, Brijesh Dongol
2022	J	`jnl`	Implementing and verifying release-acquire transactional memory in C11. Proc. ACM Program. Lang. Sadegh Dalvandi, Brijesh Dongol
2022	J	`jnl`	Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. J. Autom. Reason. Sadegh Dalvandi, Brijesh Dongol, Simon Doherty, Heike Wehrheim
2022	J	`jnl`	Introduction to the Special Section on iFM 2020. Formal Aspects Comput. Brijesh Dongol, Elena Troubitsyna
2022	J	`jnl`	Modularising Verification Of Durable Opacity. Log. Methods Comput. Sci. Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2022	—	`conf`	Proving Memory Access Violations in Isabelle/HOL. FTSCS Sharar Ahmadi, Brijesh Dongol, Matt Griffin
2022	J	`jnl`	Reasoning about Promises in Weak Memory Models with Event Structures (Extended Version). CoRR Heike Wehrheim, Lara Bargmann, Brijesh Dongol
2022	J	`jnl`	Unifying Operational Weak Memory Verification: An Axiomatic Approach. ACM Trans. Comput. Log. Simon Doherty, Sadegh Dalvandi, Brijesh Dongol, Heike Wehrheim
2022	J	`jnl`	View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version). CoRR Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson
2022	A	`conf`	View-Based Owicki-Gries Reasoning for Persistent x86-TSO. ESOP Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson
2022	B	`conf`	Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement. CONCUR Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2021	J	`jnl`	A Survey of Practical Formal Methods for Security. CoRR Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter Würtz Vinther Tran-Jørgensen, Jim Woodcock
2021	A	`conf`	Brief Announcement: On Strong Observational Refinement and Forward Simulation. DISC John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2021	B	`conf`	Checking Opacity and Durable Opacity with FDR. SEFM Brijesh Dongol, Jay Le-Papin
2021	J	`jnl`	Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras. Log. Methods Comput. Sci. Brijesh Dongol, Ian J. Hayes, Georg Struth
2021	J	`jnl`	On Strong Observational Refinement and Forward Simulation. CoRR John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2021	J	`jnl`	Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version). CoRR Daniel Wright, Mark Batty, Brijesh Dongol
2021	B	`conf`	Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies. FM Daniel Wright, Mark Batty, Brijesh Dongol
2021	J	`jnl`	Verifying C11-Style Weak Memory Libraries via Refinement. CoRR Sadegh Dalvandi, Brijesh Dongol
2021	B	`conf`	Verifying C11-style weak memory libraries. PPoPP Sadegh Dalvandi, Brijesh Dongol
2021	B	`conf`	Verifying Secure Speculation in Isabelle/HOL. FM Matt Griffin, Brijesh Dongol
2021	J	`jnl`	Verifying correctness of persistent concurrent data structures: a sound and complete method. Formal Aspects Comput. John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2020	C	`conf`	Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. FORTE Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim
2020	J	`jnl`	Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. CoRR Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim
2020	—	`ed.`	Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I FM Workshops (1) Emil Sekerinski, Nelma Moreira, José N. Oliveira, Daniel Ratiu, Riccardo Guidotti, Marie Farrell, Matt Luckcuck, Diego Marmsoler, José Creissac Campos, Troy Astarte, Laure Gonnord, Antonio Cerone, Luis Couto, Brijesh Dongol, Martin Kutrib, Pedro Monteiro, David Delmas
2020	—	`ed.`	Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part II FM Workshops (2) Emil Sekerinski, Nelma Moreira, José N. Oliveira, Daniel Ratiu, Riccardo Guidotti, Marie Farrell, Matt Luckcuck, Diego Marmsoler, José Creissac Campos, Troy Astarte, Laure Gonnord, Antonio Cerone, Luis Couto, Brijesh Dongol, Martin Kutrib, Pedro Monteiro, David Delmas
2020	B	`ed.`	Integrated Formal Methods - 16th International Conference, IFM 2020, Lugano, Switzerland, November 16-20, 2020, Proceedings IFM Brijesh Dongol, Elena Troubitsyna
2020	J	`jnl`	Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. CoRR Sadegh Dalvandi, Brijesh Dongol, Simon Doherty
2020	J	`jnl`	Modularising Verification Of Durable Opacity. CoRR Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2020	J	`jnl`	Owicki-Gries Reasoning for C11 RAR (Artifact). Dagstuhl Artifacts Ser. Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, Heike Wehrheim
2020	A	`conf`	Owicki-Gries Reasoning for C11 RAR. ECOOP Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, Heike Wehrheim
2020	J	`jnl`	Verifying C11-Style Weak Memory Libraries. CoRR Sadegh Dalvandi, Brijesh Dongol
2019	B	`conf`	Cylindric Kleene Lattices for Program Construction. MPC Brijesh Dongol, Ian J. Hayes, Larissa Meinicke, Georg Struth
2019	—	`ed.`	Formal Methods Teaching - Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 7, 2019, Proceedings FMTea Brijesh Dongol, Luigia Petre, Graeme Smith
2019	B	`conf`	Modular transactions: bounding mixed races in space and time. PPoPP Brijesh Dongol, Radha Jagadeesan, James Riely
2019	—	`conf`	Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs. FM Workshops (1) Keith Clark, Brijesh Dongol, Peter Robinson
2019	—	`conf`	Towards deductive verification of C11 programs with Event-B and ProB. FTfJP@ECOOP Mohammadsadegh Dalvandi, Brijesh Dongol
2019	B	`conf`	Verifying C11 programs operationally. PPoPP Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick
2019	B	`conf`	Verifying Correctness of Persistent Concurrent Data Structures. FM John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2018	A	`conf`	Brief Announcement: Generalising Concurrent Correctness to Weak Memory. DISC Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick
2018	J	`jnl`	Causal Linearizability: Compositionality for Partially Ordered Executions. CoRR Simon Doherty, John Derrick, Brijesh Dongol, Heike Wehrheim
2018	B	`conf`	Making Linearizability Compositional for Partially Ordered Executions. IFM Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick
2018	J	`jnl`	Mechanized proofs of opacity: a comparison of two techniques. Formal Aspects Comput. John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
2018	B	`conf`	On abstraction and compositionality for weak-memory linearisability. VMCAI Brijesh Dongol, Radha Jagadeesan, James Riely, Alasdair Armstrong
2018	—	`ed.`	Proceedings 18th Refinement Workshop, Refine@FM 2018, Oxford, UK, 18th July 2018. Refine@FM John Derrick, Brijesh Dongol, Steve Reeves
2018	J	`jnl`	Transactions in relaxed memory architectures. Proc. ACM Program. Lang. Brijesh Dongol, Radha Jagadeesan, James Riely
2018	J	`jnl`	Verifying C11 Programs Operationally. CoRR Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick
2017	—	`ch.`	A Proof Method for Linearizability on TSO Architectures. Provably Correct Systems John Derrick, Graeme Smith, Lindsay Groves, Brijesh Dongol
2017	J	`jnl`	Decidability and complexity for quiescent consistency and its variations. Inf. Comput. Brijesh Dongol, Robert M. Hierons
2017	C	`conf`	Modularising Opacity Verification for Hybrid Transactional Memory. FORTE Alasdair Armstrong, Brijesh Dongol
2017	J	`jnl`	Partial Semigroups and Convolution Algebras. Arch. Formal Proofs Brijesh Dongol, Victor B. F. Gomes, Ian J. Hayes, Georg Struth
2017	C	`conf`	Proving Opacity via Linearizability: A Sound and Complete Method. FORTE Alasdair Armstrong, Brijesh Dongol, Simon Doherty
2017	J	`jnl`	Relational Convolution, Generalised Modalities and Incidence Algebras. CoRR Brijesh Dongol, Ian J. Hayes, Georg Struth
2016	—	`conf`	An Interval Logic for Stream-Processing Functions: A Convolution-Based Construction. FTSCS Brijesh Dongol
2016	C	`conf`	Contextual Trace Refinement for Concurrent Objects: Safety and Progress. ICFEM Brijesh Dongol, Lindsay Groves
2016	J	`jnl`	Contextual trace refinement for concurrent objects: Safety and progress. CoRR Brijesh Dongol, Lindsay Groves
2016	J	`jnl`	Convolution as a Unifying Concept: Applications in Separation Logic, Interval Calculi, and Concurrency. ACM Trans. Comput. Log. Brijesh Dongol, Ian J. Hayes, Georg Struth
2016	A*	`conf`	Decidability and Complexity for Quiescent Consistency. LICS Brijesh Dongol, Robert M. Hierons
2016	B	`conf`	Proving Opacity of a Pessimistic STM. OPODIS Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim
2016	J	`jnl`	Reducing Opacity to Linearizability: A Sound and Complete Method. CoRR Alasdair Armstrong, Brijesh Dongol, Simon Doherty
2015	B	`conf`	A Program Construction and Verification Tool for Separation Logic. MPC Brijesh Dongol, Victor B. F. Gomes, Georg Struth
2015	J	`jnl`	Decidability and Complexity for Quiescent Consistency and its Variations. CoRR Brijesh Dongol, Robert M. Hierons
2015	A	`conf`	Defining Correctness Conditions for Concurrent Objects in Multicore Architectures. ECOOP Brijesh Dongol, John Derrick, Lindsay Groves, Graeme Smith
2015	J	`jnl`	Interval-based data refinement: A uniform approach to true concurrency in discrete and real-time systems. Sci. Comput. Program. Brijesh Dongol, John Derrick
2015	—	`conf`	Towards linking correctness conditions for concurrent objects and contextual trace refinement. Refine@FM Brijesh Dongol, Lindsay Groves
2015	J	`jnl`	Verifying Linearisability: A Comparative Survey. ACM Comput. Surv. Brijesh Dongol, John Derrick
2015	B	`conf`	Verifying Opacity of a Transactional Mutex Lock. FM John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
2014	—	`conf`	Admit Your Weakness: Verifying Correctness on TSO Architectures. FACS Graeme Smith, John Derrick, Brijesh Dongol
2014	J	`jnl`	Convolution, Separation and Concurrency. CoRR Brijesh Dongol, Ian J. Hayes, Georg Struth
2014	J	`jnl`	Deriving real-time action systems with multiple time bands using algebraic reasoning. Sci. Comput. Program. Brijesh Dongol, Ian J. Hayes, John Derrick
2014	J	`jnl`	Principles for Verification Tools: Separation Logic. CoRR Brijesh Dongol, Victor B. F. Gomes, Georg Struth
2014	B	`conf`	Quiescent Consistency: Defining and Verifying Relaxed Linearizability. FM John Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, Heike Wehrheim
2014	C	`conf`	Reasoning Algebraically About Refinement on TSO Architectures. ICTAC Brijesh Dongol, John Derrick, Graeme Smith
2014	J	`jnl`	Reasoning about goal-directed real-time teleo-reactive programs. Formal Aspects Comput. Brijesh Dongol, Ian J. Hayes, Peter J. Robinson
2014	—	`conf`	Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures. Haifa Verification Conference John Derrick, Graeme Smith, Lindsay Groves, Brijesh Dongol
2014	B	`conf`	Verifying Linearizability on TSO Architectures. IFM John Derrick, Graeme Smith, Brijesh Dongol
2014	J	`jnl`	Verifying linearizability: A comparative survey. CoRR Brijesh Dongol, John Derrick
2013	C	`conf`	A High-Level Semantics for Program Execution under Total Store Order Memory. ICTAC Brijesh Dongol, Oleg Travkin, John Derrick, Heike Wehrheim
2013	J	`jnl`	Comparing Degrees of Non-Determinism in Expression Evaluation. Comput. J. Ian J. Hayes, Alan Burns, Brijesh Dongol, Cliff B. Jones
2013	—	`conf`	Data refinement for true concurrency Refine@IFM Brijesh Dongol, John Derrick
2013	J	`jnl`	Deriving real-time action systems in a sampling logic. Sci. Comput. Program. Brijesh Dongol, Ian J. Hayes
2013	J	`jnl`	Simplifying proofs of linearisability using layers of abstraction. CoRR Brijesh Dongol, John Derrick
2013	J	`jnl`	Simplifying proofs of linearisability using layers of abstraction. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Brijesh Dongol, John Derrick
2012	B	`conf`	Deriving Real-Time Action Systems Controllers from Multiscale System Specifications. MPC Brijesh Dongol, Ian J. Hayes
2012	J	`jnl`	Fractional Permissions and Non-Deterministic Evaluators in Interval Temporal Logic. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Brijesh Dongol, John Derrick, Ian J. Hayes
2012	J	`jnl`	Proving linearisability via coarse-grained abstraction CoRR Brijesh Dongol, John Derrick
2012	B	`conf`	Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands. IFM Brijesh Dongol, Ian J. Hayes
2012	C	`conf`	Towards an Algebra for Real-Time Programs. RAMiCS Brijesh Dongol, Ian J. Hayes, Larissa Meinicke, Kim Solin
2011	J	`jnl`	Approximating Idealised Real-Time Specifications Using Time Bands. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Brijesh Dongol, Ian J. Hayes
2010	B	`conf`	Compositional Action System Derivation Using Enforced Properties. MPC Brijesh Dongol, Ian J. Hayes
2009	J	`jnl`	A general technique for proving lock-freedom. Sci. Comput. Program. Robert Colvin, Brijesh Dongol
2009	—	`conf`	Enforcing Safety and Progress Properties: An Approach to Concurrent Program Derivation. Australian Software Engineering Conference Brijesh Dongol, Ian J. Hayes
2009	—	`—`	Progress-based verification and derivation of concurrent programs Brijesh Dongol
2008	J	`jnl`	Streamlining progress-based derivations of concurrent programs. Formal Aspects Comput. Brijesh Dongol, Arjan J. Mooij
2007	C	`conf`	Verifying Lock-Freedom Using Well-Founded Orders. ICTAC Robert Colvin, Brijesh Dongol
2006	—	`conf`	Derivation of Java Monitors. ASWEC Brijesh Dongol
2006	J	`jnl`	Extending the theory of Owicki and Gries with a logic of progress. Log. Methods Comput. Sci. Brijesh Dongol, Doug Goldson
2006	C	`conf`	Formalising Progress Properties of Non-blocking Programs. ICFEM Brijesh Dongol
2006	B	`conf`	Progress in Deriving Concurrent Programs: Emphasizing the Role of Stable Guards. MPC Brijesh Dongol, Arjan J. Mooij
2005	—	`conf`	Concurrent Program Design in the Extended Theory of Owicki and Gries. CATS Doug Goldson, Brijesh Dongol
2005	J	`jnl`	Extending the theory of Owicki and Gries with a logic of progress CoRR Brijesh Dongol, Doug Goldson