Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates
Abstract elided by the publisher.
Related papers
- Proof Automation for Linearizability in Separation Logic OOPSLA 2023
- Mechanically verified proof obligations for linearizability TOPLAS 2011
- Deriving linearizable fine-grained concurrent objects PLDI 2008
- A Proof Recipe for Linearizability in Relaxed Memory Separation Logic PLDI 2024
- Automatically Verifying Replication-Aware Linearizability OOPSLA 2025
- A Compositional Theory of Linearizability POPL 2023
- Hoare-style specifications as correctness conditions for non-linearizable concurrent objects OOPSLA 2016
- Linearizability: A Correctness Condition for Concurrent Objects TOPLAS 1990