| Publication | Date of Publication | Type |
|---|
A verified durable transactional mutex lock for persistent x86-TSO
Formal Methods in System Design | 2025-01-13 | Paper |
Mechanised operational reasoning for C11 programs with relaxed dependencies
Formal Aspects of Computing | 2024-09-25 | Paper |
| Weak progressive forward simulation is necessary and sufficient for strong observational refinement | 2024-08-13 | Paper |
| Verifying correctness of persistent concurrent data structures | 2024-03-14 | Paper |
| Rely-guarantee reasoning for causally consistent shared memory | 2024-02-01 | Paper |
scientific article; zbMATH DE number 7774306 (Why is no real title available?)
(available as arXiv preprint) | 2023-12-08 | Paper |
A Survey of Practical Formal Methods for Security
Formal Aspects of Computing | 2023-08-31 | Paper |
Reasoning about promises in weak memory models with event structures
Formal Methods | 2023-08-17 | Paper |
Reasoning about promises in weak memory models with event structures
Formal Methods | 2023-08-17 | Paper |
Making Linearizability Compositional for Partially Ordered Executions
Lecture Notes in Computer Science | 2023-06-28 | Paper |
Making Linearizability Compositional for Partially Ordered Executions
Lecture Notes in Computer Science | 2023-06-28 | Paper |
Checking opacity and durable opacity with FDR
Software Engineering and Formal Methods | 2023-05-26 | Paper |
| Verifying Secure Speculation in Isabelle/HOL | 2023-04-21 | Paper |
Unifying Operational Weak Memory Verification: An Axiomatic Approach
ACM Transactions on Computational Logic | 2022-12-08 | Paper |
Defining and verifying durable opacity: correctness for persistent software transactional memory
Formal Techniques for Distributed Objects, Components, and Systems | 2022-10-13 | Paper |
scientific article; zbMATH DE number 7577571 (Why is no real title available?)
(available as arXiv preprint) | 2022-08-30 | Paper |
| scientific article; zbMATH DE number 7577571 (Why is no real title available?) | 2022-08-30 | Paper |
Modularising opacity verification for hybrid transactional memory
Formal Techniques for Distributed Objects, Components, and Systems | 2022-06-15 | Paper |
Proving opacity via linearizability: a sound and complete method
Formal Techniques for Distributed Objects, Components, and Systems | 2022-06-15 | Paper |
Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
Journal of Automated Reasoning | 2022-03-25 | Paper |
Verifying correctness of persistent concurrent data structures: a sound and complete method
Formal Aspects of Computing | 2021-09-14 | Paper |
Convolution algebras: relational convolution, generalised modalities and incidence algebras
(available as arXiv preprint) | 2021-03-26 | Paper |
| Convolution algebras: relational convolution, generalised modalities and incidence algebras | 2021-03-26 | Paper |
On abstraction and compositionality for weak-memory linearisability
Lecture Notes in Computer Science | 2020-07-07 | Paper |
| Cylindric Kleene lattices for program construction | 2020-05-05 | Paper |
Verifying opacity of a transactional mutex lock
FM 2015: Formal Methods | 2019-12-19 | Paper |
Mechanized proofs of opacity: a comparison of two techniques
Formal Aspects of Computing | 2018-09-12 | Paper |
| Proving opacity of a pessimistic STM | 2018-07-18 | Paper |
Decidability and complexity for quiescent consistency
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
Decidability and complexity for quiescent consistency
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
Decidability and complexity for quiescent consistency and its variations
Information and Computation | 2017-11-16 | Paper |
Convolution as a Unifying Concept
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Reasoning about goal-directed real-time teleo-reactive programs
Formal Aspects of Computing | 2016-08-05 | Paper |
A program construction and verification tool for separation logic
Lecture Notes in Computer Science | 2015-08-27 | Paper |
A program construction and verification tool for separation logic
Lecture Notes in Computer Science | 2015-08-27 | Paper |
Reasoning algebraically about refinement on TSO architectures
Theoretical Aspects of Computing – ICTAC 2014 | 2015-01-13 | Paper |
A high-level semantics for program execution under total store order memory
Theoretical Aspects of Computing – ICTAC 2013 | 2013-10-04 | Paper |
Towards an algebra for real-time programs
Relational and Algebraic Methods in Computer Science | 2012-09-21 | Paper |
Deriving Real-Time Action Systems Controllers from Multiscale System Specifications
Lecture Notes in Computer Science | 2012-09-05 | Paper |
Compositional action system derivation using enforced properties
Lecture Notes in Computer Science | 2010-07-26 | Paper |
Progress in Deriving Concurrent Programs: Emphasizing the Role of Stable Guards
Lecture Notes in Computer Science | 2009-04-02 | Paper |
A general technique for proving lock-freedom
Science of Computer Programming | 2009-02-19 | Paper |
Verifying Lock-Freedom Using Well-Founded Orders
Theoretical Aspects of Computing – ICTAC 2007 | 2008-09-17 | Paper |
Streamlining progress-based derivations of concurrent programs
Formal Aspects of Computing | 2008-04-09 | Paper |
Extending the theory of Owicki and Gries with a logic of progress
Logical Methods in Computer Science | 2007-10-11 | Paper |
