Proof Automation for Linearizability in Separation Logic
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
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.
Syllabus
[OOPSLA23] Proof Automation for Linearizability in Separation Logic
Taught by
ACM SIGPLAN
Related Courses
Verifying the LLVMStrange Loop Conference via YouTube Beweisbar sichere Software
media.ccc.de via YouTube RustBelt: A Quick Dive Into the Abyss - Formalizing Rust's Safety Story
Rust via YouTube Building Measure Theory Using Hierarchy Builder
Hausdorff Center for Mathematics via YouTube Using Formal Methods to Eliminate Exploitable Bugs - YOW! 2015
GOTO Conferences via YouTube