| Publication | Date of Publication | Type |
|---|
| A verified durable transactional mutex lock for persistent x86-TSO | 2025-01-13 | Paper |
| Mechanised operational reasoning for C11 programs with relaxed dependencies | 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 |
| https://portal.mardi4nfdi.de/entity/Q6083440 | 2023-12-08 | Paper |
| A Survey of Practical Formal Methods for Security | 2023-08-31 | Paper |
| Reasoning about promises in weak memory models with event structures | 2023-08-17 | Paper |
| Making Linearizability Compositional for Partially Ordered Executions | 2023-06-28 | Paper |
| Checking opacity and durable opacity with FDR | 2023-05-26 | Paper |
| Verifying Secure Speculation in Isabelle/HOL | 2023-04-21 | Paper |
| Unifying Operational Weak Memory Verification: An Axiomatic Approach | 2022-12-08 | Paper |
| Defining and verifying durable opacity: correctness for persistent software transactional memory | 2022-10-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5101340 | 2022-08-30 | Paper |
| Modularising opacity verification for hybrid transactional memory | 2022-06-15 | Paper |
| Proving opacity via linearizability: a sound and complete method | 2022-06-15 | Paper |
| Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL | 2022-03-25 | Paper |
| Verifying correctness of persistent concurrent data structures: a sound and complete method | 2021-09-14 | Paper |
| Convolution algebras: relational convolution, generalised modalities and incidence algebras | 2021-03-26 | Paper |
| On abstraction and compositionality for weak-memory linearisability | 2020-07-07 | Paper |
| Cylindric Kleene lattices for program construction | 2020-05-05 | Paper |
| Verifying opacity of a transactional mutex lock | 2019-12-19 | Paper |
| Mechanized proofs of opacity: a comparison of two techniques | 2018-09-12 | Paper |
| Proving opacity of a pessimistic STM | 2018-07-18 | Paper |
| Decidability and complexity for quiescent consistency | 2018-04-23 | Paper |
| Decidability and complexity for quiescent consistency and its variations | 2017-11-16 | Paper |
| Convolution as a Unifying Concept | 2017-07-12 | Paper |
| Reasoning about goal-directed real-time teleo-reactive programs | 2016-08-05 | Paper |
| A program construction and verification tool for separation logic | 2015-08-27 | Paper |
| Reasoning algebraically about refinement on TSO architectures | 2015-01-13 | Paper |
| A high-level semantics for program execution under total store order memory | 2013-10-04 | Paper |
| Towards an algebra for real-time programs | 2012-09-21 | Paper |
| Deriving Real-Time Action Systems Controllers from Multiscale System Specifications | 2012-09-05 | Paper |
| Compositional action system derivation using enforced properties | 2010-07-26 | Paper |
| Progress in Deriving Concurrent Programs: Emphasizing the Role of Stable Guards | 2009-04-02 | Paper |
| A general technique for proving lock-freedom | 2009-02-19 | Paper |
| Verifying Lock-Freedom Using Well-Founded Orders | 2008-09-17 | Paper |
| Streamlining progress-based derivations of concurrent programs | 2008-04-09 | Paper |
| Extending the theory of Owicki and Gries with a logic of progress | 2007-10-11 | Paper |
