A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
Explore a groundbreaking 21-minute conference talk from POPL 2024 introducing a universal, sound, and complete proof method for machine-verifiable proofs of linearizability and strong linearizability. Delve into the innovative approach presented by researchers from Dartmouth College, Google Research, Boston University, and Microsoft, which works for any object type and ensures both soundness and completeness. Witness the method's application in proving linearizability for the Herlihy-Wing queue and Jayanti's single-scanner snapshot, as well as strong linearizability of the Jayanti-Tarjan union-find object. Learn how these proofs are machine-verified using TLAPS (TLA+ Proof System). Gain insights into this powerful technique that advances the field of verification and linearizability in concurrent systems.