Poling: SMT Aided Linearizability Proofs
Abstract elided by the publisher.
Related papers
- Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits OOPSLA 2025
- Raven: An SMT-Based Concurrency Verifier CAV 2025
- SpaceSearch: a library for building and verifying solver-aided tools ICFP 2017
- Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates CAV 2013
- Simplifying Linearizability Proofs with Reduction and Abstraction TACAS 2010
- A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability POPL 2024
- nekton: A Linearizability Proof Checker CAV 2023
- Mechanically verified proof obligations for linearizability TOPLAS 2011