| 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 |
| https://portal.mardi4nfdi.de/entity/Q5856417 | 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 |
