| Publication | Date of Publication | Type |
|---|
Liveness and latency of Byzantine state-machine replication
Distributed Computing | 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
Distributed Computing | 2022-12-09 | Paper |
| Multi-shot distributed transaction commit | 2022-07-21 | Paper |
scientific article; zbMATH DE number 7561445 (Why is no real title available?)
(available as arXiv preprint) | 2022-07-21 | Paper |
Multi-shot distributed transaction commit
Distributed Computing | 2021-09-06 | Paper |
Multi-shot distributed transaction commit
Distributed Computing | 2021-09-06 | Paper |
Specification and space complexity of collaborative text editing
Theoretical Computer Science | 2021-01-25 | Paper |
Reconfigurable Atomic Transaction Commit
Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing | 2021-01-20 | Paper |
| Algebraic laws for weak consistency | 2020-05-27 | Paper |
A generic logic for proving linearizability
(available as arXiv preprint) | 2020-01-03 | Paper |
Paxos consensus, deconstructed and abstracted
(available as arXiv preprint) | 2019-09-13 | Paper |
Compositional verification of compiler optimisations on relaxed memory
(available as arXiv preprint) | 2019-09-13 | Paper |
| Compositional verification of compiler optimisations on relaxed memory | 2019-09-13 | Paper |
Analysing snapshot isolation
Journal of the ACM | 2018-12-06 | Paper |
| Transaction chopping for parallel snapshot isolation | 2018-08-24 | Paper |
Characterizing Transactional Memory Consistency Conditions Using Observational Refinement
Journal of the ACM | 2018-08-02 | Paper |
| Robustness against consistency models with atomic visibility | 2018-03-21 | Paper |
Specification and complexity of collaborative text editing
Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing | 2017-09-29 | Paper |
Analysing snapshot isolation
Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing | 2017-09-29 | Paper |
| A framework for transactional consistency models with atomic visibility | 2017-09-12 | Paper |
Proving linearizability using partial orders
Programming Languages and Systems | 2017-05-19 | Paper |
'Cause I'm strong enough: reasoning about consistency choices in distributed systems
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2016-10-24 | Paper |
Precision and the conjunction rule in concurrent separation logic
Electronic Notes in Theoretical Computer Science | 2016-07-15 | Paper |
Composite replicated data types
Programming Languages and Systems | 2016-04-26 | Paper |
Proving that non-blocking algorithms don't block
Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-07-03 | Paper |
Modular verification of preemptive OS kernels
Proceedings of the 16th ACM SIGPLAN international conference on Functional programming | 2015-03-05 | Paper |
A programming language perspective on transactional memory consistency
Proceedings of the 2013 ACM symposium on Principles of distributed computing | 2015-03-02 | Paper |
Library abstraction for C/C++ concurrency
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-11-27 | Paper |
Proving that programs eventually do something good
Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-09-12 | Paper |
Parameterised linearisability
Automata, Languages, and Programming | 2014-07-01 | Paper |
Replicated data types, specification, verification, optimality
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
Modular verification of preemptive OS kernels
Journal of Functional Programming | 2014-02-27 | Paper |
| Towards an independent semantics and verification technology for the HLPSL specification language | 2013-09-26 | Paper |
Linearizability with ownership transfer
Logical Methods in Computer Science | 2013-09-26 | Paper |
Verifying concurrent memory reclamation algorithms with grace
Programming Languages and Systems | 2013-08-05 | Paper |
Show no weakness: sequentially consistent specifications of TSO libraries
Lecture Notes in Computer Science | 2013-03-13 | Paper |
Linearizability with ownership transfer
Lecture Notes in Computer Science | 2012-09-25 | Paper |
Concurrent Library Correctness on the TSO Memory Model
Programming Languages and Systems | 2012-06-22 | Paper |
Liveness-Preserving Atomicity Abstraction
Automata, Languages and Programming | 2011-07-07 | Paper |
Interprocedural Shape Analysis with Separated Heap Abstractions
Static Analysis | 2009-03-12 | Paper |
Local Reasoning for Storable Locks and Threads
Programming Languages and Systems | 2008-05-15 | Paper |
