Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBrijesh 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
- 2023
[c47]Heike Wehrheim
, Lara Bargmann, Brijesh Dongol:
Reasoning About Promises in Weak Memory Models with Event Structures. FM 2023: 282-300- [i24]Ori Lahav, Brijesh Dongol, Heike Wehrheim:
Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version). CoRR abs/2305.08486 (2023) - 2022
- [j27]Brijesh Dongol, Elena Troubitsyna:
Introduction to the Special Section on iFM 2020. Formal Aspects Comput. 34(1): 1 (2022) - [j26]Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter W. V. Tran-Jørgensen, Jim Woodcock:
A Survey of Practical Formal Methods for Security. Formal Aspects Comput. 34(1): 1-39 (2022) - [j25]Tsz Yiu Lam, Brijesh Dongol:
A blockchain-enabled e-learning platform. Interact. Learn. Environ. 30(7): 1229-1251 (2022) - [j24]Sadegh Dalvandi, Brijesh Dongol, Simon Doherty, Heike Wehrheim:
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, Gerhard Schellhorn, Heike Wehrheim:
Modularising Verification Of Durable Opacity. Log. Methods Comput. Sci. 18(3) (2022) - [j22]Sadegh Dalvandi, Brijesh Dongol:
Implementing and verifying release-acquire transactional memory in C11. Proc. ACM Program. Lang. 6(OOPSLA2): 1817-1844 (2022) - [j21]Simon Doherty, Sadegh Dalvandi, Brijesh Dongol, Heike Wehrheim:
Unifying Operational Weak Memory Verification: An Axiomatic Approach. ACM Trans. Comput. Log. 23(4): 27:1-27:39 (2022) - [c46]Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim:
Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement. CONCUR 2022: 31:1-31:23 - [c45]Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson:
View-Based Owicki-Gries Reasoning for Persistent x86-TSO. ESOP 2022: 234-261 - [c44]Sharar Ahmadi, Brijesh Dongol, Matt Griffin:
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, Gerhard Schellhorn, Heike Wehrheim:
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, Brijesh Dongol:
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, Jay Le-Papin:
Checking Opacity and Durable Opacity with FDR. SEFM 2021: 222-242 - [c39]John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim:
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, Heike Wehrheim:
Owicki-Gries Reasoning for C11 RAR (Artifact). Dagstuhl Artifacts Ser. 6(2): 15:1-15:2 (2020) - [c38]Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, Heike Wehrheim:
Owicki-Gries Reasoning for C11 RAR. ECOOP 2020: 11:1-11:26 - [c37]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: 39-58 - [e5]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:
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, 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:
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, Elena Troubitsyna:
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, Brijesh Dongol:
Towards deductive verification of C11 programs with Event-B and ProB. FTfJP@ECOOP 2019: 4:1-4:7 - [c35]John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim:
Verifying Correctness of Persistent Concurrent Data Structures. FM 2019: 179-195 - [c34]Keith Clark, Brijesh Dongol, Peter Robinson:
Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs. FM Workshops (1) 2019: 265-280 - [c33]Brijesh Dongol, Ian J. Hayes, Larissa Meinicke, Georg Struth:
Cylindric Kleene Lattices for Program Construction. MPC 2019: 197-225 - [c32]Brijesh Dongol, Radha Jagadeesan, James Riely:
Modular transactions: bounding mixed races in space and time. PPoPP 2019: 82-93 - [c31]Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick:
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, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim:
Mechanized proofs of opacity: a comparison of two techniques. Formal Aspects Comput. 30(5): 597-625 (2018) - [j16]Brijesh Dongol, Radha Jagadeesan, James Riely:
Transactions in relaxed memory architectures. Proc. ACM Program. Lang. 2(POPL): 18:1-18:29 (2018) - [c30]Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick:
Making Linearizability Compositional for Partially Ordered Executions. IFM 2018: 110-129 - [c29]Brijesh Dongol, Radha Jagadeesan, James Riely, Alasdair Armstrong:
On abstraction and compositionality for weak-memory linearisability. VMCAI 2018: 183-204 - [c28]Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick:
Brief Announcement: Generalising Concurrent Correctness to Weak Memory. DISC 2018: 45:1-45:3 - [e1]John Derrick, Brijesh Dongol, Steve Reeves:
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, Robert M. Hierons:
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, Simon Doherty:
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, Ian J. Hayes, Georg Struth:
Relational Convolution, Generalised Modalities and Incidence Algebras. CoRR abs/1702.04603 (2017) - 2016
- [j13]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): 15 (2016) - [c25]Brijesh Dongol:
An Interval Logic for Stream-Processing Functions: A Convolution-Based Construction. FTSCS 2016: 20-35 - [c24]Brijesh Dongol, Lindsay Groves:
Contextual Trace Refinement for Concurrent Objects: Safety and Progress. ICFEM 2016: 261-278 - [c23]Brijesh Dongol, Robert M. Hierons:
Decidability and Complexity for Quiescent Consistency. LICS 2016: 116-125 - [c22]Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim:
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, John Derrick:
Verifying Linearisability: A Comparative Survey. ACM Comput. Surv. 48(2): 19:1-19:43 (2015) - [j11]Brijesh Dongol, John Derrick:
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, John Derrick, Lindsay Groves, Graeme Smith:
Defining Correctness Conditions for Concurrent Objects in Multicore Architectures. ECOOP 2015: 470-494 - [c20]John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim:
Verifying Opacity of a Transactional Mutex Lock. FM 2015: 161-177 - [c19]Brijesh Dongol, Victor B. F. Gomes, Georg Struth:
A Program Construction and Verification Tool for Separation Logic. MPC 2015: 137-158 - [c18]Brijesh Dongol, Lindsay Groves:
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, Ian J. Hayes, Peter J. Robinson:
Reasoning about goal-directed real-time teleo-reactive programs. Formal Aspects Comput. 26(3): 563-589 (2014) - [j9]Brijesh Dongol, Ian J. Hayes, John Derrick:
Deriving real-time action systems with multiple time bands using algebraic reasoning. Sci. Comput. Program. 85: 137-165 (2014) - [c17]Graeme Smith, John Derrick, Brijesh Dongol:
Admit Your Weakness: Verifying Correctness on TSO Architectures. FACS 2014: 364-383 - [c16]John Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, Heike Wehrheim:
Quiescent Consistency: Defining and Verifying Relaxed Linearizability. FM 2014: 200-214 - [c15]John Derrick, Graeme Smith, Lindsay Groves, Brijesh Dongol:
Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures. Haifa Verification Conference 2014: 1-16 - [c14]Brijesh Dongol, John Derrick, Graeme Smith:
Reasoning Algebraically About Refinement on TSO Architectures. ICTAC 2014: 151-168 - [c13]John Derrick, Graeme Smith, Brijesh Dongol:
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, Alan Burns, Brijesh Dongol, Cliff B. Jones:
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, Ian J. Hayes:
Deriving real-time action systems in a sampling logic. Sci. Comput. Program. 78(11): 2047-2063 (2013) - [c12]Brijesh Dongol, Oleg Travkin, John Derrick, Heike Wehrheim:
A High-Level Semantics for Program Execution under Total Store Order Memory. ICTAC 2013: 177-194 - [c11]Brijesh Dongol, John Derrick:
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, Ian J. Hayes, Larissa Meinicke, Kim Solin:
Towards an Algebra for Real-Time Programs. RAMiCS 2012: 50-65 - [c9]Brijesh Dongol, Ian J. Hayes:
Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands. IFM 2012: 39-53 - [c8]Brijesh Dongol, Ian J. Hayes:
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, Ian J. Hayes:
Compositional Action System Derivation Using Enforced Properties. MPC 2010: 119-139
2000 – 2009
- 2009
- [j3]Robert Colvin, Brijesh Dongol:
A general technique for proving lock-freedom. Sci. Comput. Program. 74(3): 143-165 (2009) - [c6]Brijesh Dongol, Ian J. Hayes:
Enforcing Safety and Progress Properties: An Approach to Concurrent Program Derivation. Australian Software Engineering Conference 2009: 3-12 - 2008
- [j2]Brijesh Dongol, Arjan J. Mooij:
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, Doug Goldson:
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, Arjan J. Mooij:
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
a service of 
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).
load content from web.archive.org
Privacy notice: By enabling the option above, your browser will contact the API of web.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 2023-05-18 23:22 CEST 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:
