YoVDO

Proof Automation for Linearizability in Separation Logic

Offered By: ACM SIGPLAN via YouTube

Tags

Concurrent Programming Courses Coq Courses

Course Description

Overview

Save Big on Coursera Plus. 7,000+ courses at $160 off. Limited Time Only!
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 LLVM
Strange 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