| Publication | Date of Publication | Type |
|---|
| Liveness and latency of Byzantine state-machine replication | 2024-07-26 | Paper |
| Making Byzantine consensus live | 2023-11-02 | Paper |
| Consistency models with global operation sequencing and their composition | 2023-02-03 | Paper |
| Privatization-safe transactional memories | 2023-02-03 | Paper |
| Making Byzantine consensus live | 2022-12-09 | Paper |
| Multi-shot distributed transaction commit | 2022-07-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5091091 | 2022-07-21 | Paper |
| Multi-shot distributed transaction commit | 2021-09-06 | Paper |
| Specification and space complexity of collaborative text editing | 2021-01-25 | Paper |
| Reconfigurable Atomic Transaction Commit | 2021-01-20 | Paper |
| Algebraic laws for weak consistency | 2020-05-27 | Paper |
| A generic logic for proving linearizability | 2020-01-03 | Paper |
| Paxos consensus, deconstructed and abstracted | 2019-09-13 | Paper |
| Compositional verification of compiler optimisations on relaxed memory | 2019-09-13 | Paper |
| Analysing snapshot isolation | 2018-12-06 | Paper |
| Transaction chopping for parallel snapshot isolation | 2018-08-24 | Paper |
| Characterizing Transactional Memory Consistency Conditions Using Observational Refinement | 2018-08-02 | Paper |
| Robustness against consistency models with atomic visibility | 2018-03-21 | Paper |
| Specification and complexity of collaborative text editing | 2017-09-29 | Paper |
| Analysing snapshot isolation | 2017-09-29 | Paper |
| A framework for transactional consistency models with atomic visibility | 2017-09-12 | Paper |
| Proving linearizability using partial orders | 2017-05-19 | Paper |
| 'Cause I'm strong enough: reasoning about consistency choices in distributed systems | 2016-10-24 | Paper |
| Precision and the conjunction rule in concurrent separation logic | 2016-07-15 | Paper |
| Composite replicated data types | 2016-04-26 | Paper |
| Proving that non-blocking algorithms don't block | 2015-07-03 | Paper |
| Modular verification of preemptive OS kernels | 2015-03-05 | Paper |
| A programming language perspective on transactional memory consistency | 2015-03-02 | Paper |
| Library abstraction for C/C++ concurrency | 2014-11-27 | Paper |
| Proving that programs eventually do something good | 2014-09-12 | Paper |
| Parameterised linearisability | 2014-07-01 | Paper |
| Replicated data types, specification, verification, optimality | 2014-04-10 | Paper |
| Modular verification of preemptive OS kernels | 2014-02-27 | Paper |
| Towards an independent semantics and verification technology for the HLPSL specification language | 2013-09-26 | Paper |
| Linearizability with ownership transfer | 2013-09-26 | Paper |
| Verifying concurrent memory reclamation algorithms with grace | 2013-08-05 | Paper |
| Show no weakness: sequentially consistent specifications of TSO libraries | 2013-03-13 | Paper |
| Linearizability with ownership transfer | 2012-09-25 | Paper |
| Concurrent Library Correctness on the TSO Memory Model | 2012-06-22 | Paper |
| Liveness-Preserving Atomicity Abstraction | 2011-07-07 | Paper |
| Interprocedural Shape Analysis with Separated Heap Abstractions | 2009-03-12 | Paper |
| Local Reasoning for Storable Locks and Threads | 2008-05-15 | Paper |
