Proof Automation for Linearizability in Separation Logic

Explore a 19-minute video presentation from OOPSLA 2023 on proof automation for linearizability in separation logic. Delve into recent advances in concurrent separation logic and their impact on formal verification of fine-grained concurrent programs. Learn about compositional approaches to linearizability, including contextual refinement and logical atomicity, and how they enable proving linearizability of whole programs or compound data structures. Discover the key ingredients of proof automation developed by the presenters, including proof rules directed by both program and logical state. Examine the implementation of this automation in Coq through the extension of Diaframe, and understand how it significantly reduces proof work for linearizability approaches. Gain insights into the evaluation of this proof automation on existing benchmarks and novel proofs, demonstrating its effectiveness in simplifying complex verification tasks.