default search action
Brijesh Dongol
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j32]Brijesh Dongol, Matthew Griffin, Andrei Popescu, Jamie Wright:
Secret-Directed Unwinding. Arch. Formal Proofs 2024 (2024) - [j31]Maurice H. ter Beek, Manfred Broy, Brijesh Dongol:
The Role of Formal Methods in Computer Science Education. Inroads 15(4): 58-66 (2024) - [j30]Guillaume Ambal
, Brijesh Dongol
Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures. Proc. ACM Program. Lang. 8(OOPSLA2): 1982-2009 (2024) - [j29]Sharar Ahmadi, Brijesh Dongol, Matt Griffin
Operationally proving memory access violations in Isabelle/HOL. Sci. Comput. Program. 234: 103088 (2024) - [c58]Brijesh Dongol, Matt Griffin, Andrei Popescu, Jamie Wright:
Relative Security: Formally Modeling and (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities. CSF 2024: 403-418 - [c57]Azalea Raad
Intel PMDK Transactions: Specification, Validation and Concurrency. ESOP (2) 2024: 150-179 - [c56]Azalea Raad
Artifact Report: Intel PMDK Transactions: Specification, Validation and Concurrency. ESOP (2) 2024: 180-184 - [c55]Lara Bargmann
Unifying Weak Memory Verification Using Potentials. FM (1) 2024: 519-537 - [c54]Sergey Egorov, Gregory V. Chockler, Brijesh Dongol, Dan O'Keeffe, Sadegh Keshavarzi:
Mangosteen: Fast Transparent Durability for Linearizable Applications using NVM. USENIX ATC 2024: 799-815 - [c53]Stefan Bodenmüller
A Fully Verified Persistency Library. VMCAI (2) 2024: 26-47 - [c52]Armando Castañeda, Gregory V. Chockler, Brijesh Dongol, Ori Lahav:
What Cannot Be Implemented on Weak Memory? DISC 2024: 11:1-11:22 - [i27]Armando Castañeda, Gregory V. Chockler, Brijesh Dongol, Ori Lahav:
What Cannot Be Implemented on Weak Memory? CoRR abs/2405.16611 (2024) - [i26]Sharar Ahmadi, Jay Le-Papin, Liqun Chen, Brijesh Dongol, Sasa Radomirovic, Helen Treharne:
On the Design and Security of Collective Remote Attestation Protocols. CoRR abs/2407.09203 (2024) - 2023
- [j28]Daniel Wright
Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies. Formal Aspects Comput. 35(2): 10:1-10:27 (2023) - [c51]Ori Lahav
Rely-Guarantee Reasoning for Causally Consistent Shared Memory. CAV (1) 2023: 206-229 - [c50]Heike Wehrheim
Reasoning About Promises in Weak Memory Models with Event Structures. FM 2023: 282-300 - [c49]Mikhail Semenyuk
Ownership-Based Owicki-Gries Reasoning. SAC 2023: 1685-1694 - [c48]Mikhail Semenyuk
Verifying Read-Copy Update Under RC11. SEFM 2023: 301-319 - [c47]Jay Le-Papin
Verifying List Swarm Attestation Protocols. WISEC 2023: 163-174 - [i25]Ori Lahav, Brijesh Dongol
Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version). CoRR abs/2305.08486 (2023) - [i24]Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol:
Intel PMDK Transactions: Specification, Validation and Concurrency (Extended Version). CoRR abs/2312.13828 (2023) - 2022
- [j27]Brijesh Dongol
Introduction to the Special Section on iFM 2020. Formal Aspects Comput. 34(1): 1 (2022) - [j26]Tomas Kulik
A Survey of Practical Formal Methods for Security. Formal Aspects Comput. 34(1): 1-39 (2022) - [j25]Tsz Yiu Lam
A blockchain-enabled e-learning platform. Interact. Learn. Environ. 30(7): 1229-1251 (2022) - [j24]Sadegh Dalvandi
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. J. Autom. Reason. 66(1): 141-171 (2022) - [j23]Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol
Modularising Verification Of Durable Opacity. Log. Methods Comput. Sci. 18(3) (2022) - [j22]Sadegh Dalvandi
Implementing and verifying release-acquire transactional memory in C11. Proc. ACM Program. Lang. 6(OOPSLA2): 1817-1844 (2022) - [j21]Simon Doherty
Unifying Operational Weak Memory Verification: An Axiomatic Approach. ACM Trans. Comput. Log. 23(4): 27:1-27:39 (2022) - [c46]Brijesh Dongol
Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement. CONCUR 2022: 31:1-31:23 - [c45]Eleni Vafeiadi Bila
View-Based Owicki-Gries Reasoning for Persistent x86-TSO. ESOP 2022: 234-261 - [c44]Sharar Ahmadi, Brijesh Dongol
Proving Memory Access Violations in Isabelle/HOL. FTSCS 2022: 45-55 - [i23]Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson:
View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version). CoRR abs/2201.05860 (2022) - [i22]Sadegh Dalvandi, Brijesh Dongol
Implementing and Verifying Release-Acquire Transactional Memory (Extended Version). CoRR abs/2208.00315 (2022) - [i21]Heike Wehrheim, Lara Bargmann, Brijesh Dongol:
Reasoning about Promises in Weak Memory Models with Event Structures (Extended Version). CoRR abs/2211.16330 (2022) - 2021
- [j20]John Derrick, Simon Doherty, Brijesh Dongol
Verifying correctness of persistent concurrent data structures: a sound and complete method. Formal Aspects Comput. 33(4-5): 547-573 (2021) - [j19]Brijesh Dongol, Ian J. Hayes, Georg Struth:
Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras. Log. Methods Comput. Sci. 17(1) (2021) - [c43]Matt Griffin
Verifying Secure Speculation in Isabelle/HOL. FM 2021: 43-60 - [c42]Daniel Wright, Mark Batty, Brijesh Dongol
Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies. FM 2021: 237-254 - [c41]Sadegh Dalvandi, Brijesh Dongol
Verifying C11-style weak memory libraries. PPoPP 2021: 451-453 - [c40]Brijesh Dongol
Checking Opacity and Durable Opacity with FDR. SEFM 2021: 222-242 - [c39]John Derrick
Brief Announcement: On Strong Observational Refinement and Forward Simulation. DISC 2021: 55:1-55:4 - [i20]John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim:
On Strong Observational Refinement and Forward Simulation. CoRR abs/2107.14509 (2021) - [i19]Daniel Wright, Mark Batty, Brijesh Dongol:
Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version). CoRR abs/2108.01418 (2021) - [i18]Sadegh Dalvandi, Brijesh Dongol:
Verifying C11-Style Weak Memory Libraries via Refinement. CoRR abs/2108.06944 (2021) - [i17]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 abs/2109.01362 (2021) - 2020
- [j18]Sadegh Dalvandi, Simon Doherty, Brijesh Dongol
Owicki-Gries Reasoning for C11 RAR (Artifact). Dagstuhl Artifacts Ser. 6(2): 15:1-15:2 (2020) - [c38]Sadegh Dalvandi
Owicki-Gries Reasoning for C11 RAR. ECOOP 2020: 11:1-11:26 - [c37]Eleni Bila, Simon Doherty, Brijesh Dongol
Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. FORTE 2020: 39-58 - [e5]Emil Sekerinski
Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I. Lecture Notes in Computer Science 12232, Springer 2020, ISBN 978-3-030-54993-0 [contents] - [e4]Emil Sekerinski
Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part II. Lecture Notes in Computer Science 12233, Springer 2020, ISBN 978-3-030-54996-1 [contents] - [e3]Brijesh Dongol
Integrated Formal Methods - 16th International Conference, IFM 2020, Lugano, Switzerland, November 16-20, 2020, Proceedings. Lecture Notes in Computer Science 12546, Springer 2020, ISBN 978-3-030-63460-5 [contents] - [i16]Sadegh Dalvandi, Brijesh Dongol, Simon Doherty:
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. CoRR abs/2004.02983 (2020) - [i15]Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim:
Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. CoRR abs/2004.08200 (2020) - [i14]Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim:
Modularising Verification Of Durable Opacity. CoRR abs/2011.15013 (2020) - [i13]Sadegh Dalvandi, Brijesh Dongol:
Verifying C11-Style Weak Memory Libraries. CoRR abs/2012.14133 (2020)
2010 – 2019
- 2019
- [c36]Mohammadsadegh Dalvandi
Towards deductive verification of C11 programs with Event-B and ProB. FTfJP@ECOOP 2019: 4:1-4:7 - [c35]John Derrick
Verifying Correctness of Persistent Concurrent Data Structures. FM 2019: 179-195 - [c34]Keith Clark, Brijesh Dongol
Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs. FM Workshops (1) 2019: 265-280 - [c33]Brijesh Dongol
Cylindric Kleene Lattices for Program Construction. MPC 2019: 197-225 - [c32]Brijesh Dongol
Modular transactions: bounding mixed races in space and time. PPoPP 2019: 82-93 - [c31]Simon Doherty, Brijesh Dongol
Verifying C11 programs operationally. PPoPP 2019: 355-365 - [e2]Brijesh Dongol, Luigia Petre, Graeme Smith:
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. Lecture Notes in Computer Science 11758, Springer 2019, ISBN 978-3-030-32440-7 [contents] - 2018
- [j17]John Derrick
Mechanized proofs of opacity: a comparison of two techniques. Formal Aspects Comput. 30(5): 597-625 (2018) - [j16]Brijesh Dongol
Transactions in relaxed memory architectures. Proc. ACM Program. Lang. 2(POPL): 18:1-18:29 (2018) - [c30]Simon Doherty, Brijesh Dongol
Making Linearizability Compositional for Partially Ordered Executions. IFM 2018: 110-129 - [c29]Brijesh Dongol
On abstraction and compositionality for weak-memory linearisability. VMCAI 2018: 183-204 - [c28]Simon Doherty, Brijesh Dongol
Brief Announcement: Generalising Concurrent Correctness to Weak Memory. DISC 2018: 45:1-45:3 - [e1]John Derrick
Proceedings 18th Refinement Workshop, Refine@FM 2018, Oxford, UK, 18th July 2018. EPTCS 282, 2018 [contents] - [i12]Simon Doherty, John Derrick, Brijesh Dongol, Heike Wehrheim:
Causal Linearizability: Compositionality for Partially Ordered Executions. CoRR abs/1802.01866 (2018) - [i11]Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick:
Verifying C11 Programs Operationally. CoRR abs/1811.09143 (2018) - 2017
- [j15]Brijesh Dongol, Victor B. F. Gomes, Ian J. Hayes, Georg Struth:
Partial Semigroups and Convolution Algebras. Arch. Formal Proofs 2017 (2017) - [j14]Brijesh Dongol
Decidability and complexity for quiescent consistency and its variations. Inf. Comput. 257: 1-21 (2017) - [c27]Alasdair Armstrong, Brijesh Dongol
Modularising Opacity Verification for Hybrid Transactional Memory. FORTE 2017: 33-49 - [c26]Alasdair Armstrong, Brijesh Dongol
Proving Opacity via Linearizability: A Sound and Complete Method. FORTE 2017: 50-66 - [p1]John Derrick, Graeme Smith, Lindsay Groves, Brijesh Dongol:
A Proof Method for Linearizability on TSO Architectures. Provably Correct Systems 2017: 61-91 - [i10]Brijesh Dongol
Relational Convolution, Generalised Modalities and Incidence Algebras. CoRR abs/1702.04603 (2017) - 2016
- [j13]Brijesh Dongol
Convolution as a Unifying Concept: Applications in Separation Logic, Interval Calculi, and Concurrency. ACM Trans. Comput. Log. 17(3): 15 (2016) - [c25]Brijesh Dongol
An Interval Logic for Stream-Processing Functions: A Convolution-Based Construction. FTSCS 2016: 20-35 - [c24]Brijesh Dongol
Contextual Trace Refinement for Concurrent Objects: Safety and Progress. ICFEM 2016: 261-278 - [c23]Brijesh Dongol
Decidability and Complexity for Quiescent Consistency. LICS 2016: 116-125 - [c22]Simon Doherty, Brijesh Dongol
Proving Opacity of a Pessimistic STM. OPODIS 2016: 35:1-35:17 - [i9]Brijesh Dongol, Lindsay Groves:
Contextual trace refinement for concurrent objects: Safety and progress. CoRR abs/1603.01412 (2016) - [i8]Alasdair Armstrong, Brijesh Dongol, Simon Doherty:
Reducing Opacity to Linearizability: A Sound and Complete Method. CoRR abs/1610.01004 (2016) - 2015
- [j12]Brijesh Dongol
Verifying Linearisability: A Comparative Survey. ACM Comput. Surv. 48(2): 19:1-19:43 (2015) - [j11]Brijesh Dongol
Interval-based data refinement: A uniform approach to true concurrency in discrete and real-time systems. Sci. Comput. Program. 111: 214-247 (2015) - [c21]Brijesh Dongol
Defining Correctness Conditions for Concurrent Objects in Multicore Architectures. ECOOP 2015: 470-494 - [c20]John Derrick
Verifying Opacity of a Transactional Mutex Lock. FM 2015: 161-177 - [c19]Brijesh Dongol
A Program Construction and Verification Tool for Separation Logic. MPC 2015: 137-158 - [c18]Brijesh Dongol
Towards linking correctness conditions for concurrent objects and contextual trace refinement. Refine@FM 2015: 107-111 - [i7]Brijesh Dongol, Robert M. Hierons
Decidability and Complexity for Quiescent Consistency and its Variations. CoRR abs/1511.08447 (2015) - 2014
- [j10]Brijesh Dongol
Reasoning about goal-directed real-time teleo-reactive programs. Formal Aspects Comput. 26(3): 563-589 (2014) - [j9]Brijesh Dongol
Deriving real-time action systems with multiple time bands using algebraic reasoning. Sci. Comput. Program. 85: 137-165 (2014) - [c17]Graeme Smith
Admit Your Weakness: Verifying Correctness on TSO Architectures. FACS 2014: 364-383 - [c16]John Derrick
Quiescent Consistency: Defining and Verifying Relaxed Linearizability. FM 2014: 200-214 - [c15]John Derrick, Graeme Smith
Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures. Haifa Verification Conference 2014: 1-16 - [c14]Brijesh Dongol
Reasoning Algebraically About Refinement on TSO Architectures. ICTAC 2014: 151-168 - [c13]John Derrick
Verifying Linearizability on TSO Architectures. IFM 2014: 341-356 - [i6]Brijesh Dongol, Ian J. Hayes, Georg Struth:
Convolution, Separation and Concurrency. CoRR abs/1410.4235 (2014) - [i5]Brijesh Dongol, Victor B. F. Gomes, Georg Struth:
Principles for Verification Tools: Separation Logic. CoRR abs/1410.4439 (2014) - [i4]Brijesh Dongol, John Derrick:
Verifying linearizability: A comparative survey. CoRR abs/1410.6268 (2014) - 2013
- [j8]Ian J. Hayes
Comparing Degrees of Non-Determinism in Expression Evaluation. Comput. J. 56(6): 741-755 (2013) - [j7]Brijesh Dongol, John Derrick:
Simplifying proofs of linearisability using layers of abstraction. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 66 (2013) - [j6]Brijesh Dongol
Deriving real-time action systems in a sampling logic. Sci. Comput. Program. 78(11): 2047-2063 (2013) - [c12]Brijesh Dongol
A High-Level Semantics for Program Execution under Total Store Order Memory. ICTAC 2013: 177-194 - [c11]Brijesh Dongol
Data refinement for true concurrency. Refine@IFM 2013: 15-35 - [i3]Brijesh Dongol, John Derrick:
Simplifying proofs of linearisability using layers of abstraction. CoRR abs/1307.6958 (2013) - 2012
- [j5]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) - [c10]Brijesh Dongol
Towards an Algebra for Real-Time Programs. RAMiCS 2012: 50-65 - [c9]Brijesh Dongol
Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands. IFM 2012: 39-53 - [c8]Brijesh Dongol
Deriving Real-Time Action Systems Controllers from Multiscale System Specifications. MPC 2012: 102-131 - [i2]Brijesh Dongol, John Derrick:
Proving linearisability via coarse-grained abstraction. CoRR abs/1212.5116 (2012) - 2011
- [j4]Brijesh Dongol, Ian J. Hayes:
Approximating Idealised Real-Time Specifications Using Time Bands. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 46 (2011) - 2010
- [c7]Brijesh Dongol
Compositional Action System Derivation Using Enforced Properties. MPC 2010: 119-139
2000 – 2009
- 2009
- [b1]Brijesh Dongol:
Progress-based verification and derivation of concurrent programs. University of Queensland, Australia, 2009 - [j3]Robert Colvin
A general technique for proving lock-freedom. Sci. Comput. Program. 74(3): 143-165 (2009) - [c6]Brijesh Dongol
Enforcing Safety and Progress Properties: An Approach to Concurrent Program Derivation. Australian Software Engineering Conference 2009: 3-12 - 2008
- [j2]Brijesh Dongol
Streamlining progress-based derivations of concurrent programs. Formal Aspects Comput. 20(2): 141-160 (2008) - 2007
- [c5]Robert Colvin, Brijesh Dongol
Verifying Lock-Freedom Using Well-Founded Orders. ICTAC 2007: 124-138 - 2006
- [j1]Brijesh Dongol
Extending the theory of Owicki and Gries with a logic of progress. Log. Methods Comput. Sci. 2(1) (2006) - [c4]Brijesh Dongol
Derivation of Java Monitors. ASWEC 2006: 211-220 - [c3]Brijesh Dongol
Formalising Progress Properties of Non-blocking Programs. ICFEM 2006: 284-303 - [c2]Brijesh Dongol
Progress in Deriving Concurrent Programs: Emphasizing the Role of Stable Guards. MPC 2006: 140-161 - 2005
- [c1]Doug Goldson, Brijesh Dongol:
Concurrent Program Design in the Extended Theory of Owicki and Gries. CATS 2005: 41-50 - [i1]Brijesh Dongol, Doug Goldson:
Extending the theory of Owicki and Gries with a logic of progress. CoRR abs/cs/0512012 (2005)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-10 20:51 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: