Compositional Verification of Concurrent C Programs with Search Structure Templat...
summary
Implements Krishna et al.’s search-structure templates inside Verified Software Toolchain (VST) to prove C implementations of fine-grained concurrent search trees; verifies two templates (lock coupling and give up template) and one binary search tree, translating recursive proofs to loop invariants and handling C realities like integer overflow. Most proof effort concentrates on Traverse and loop invariants; maintenance (deletion/rotations) and template-data coupling still require per–combination work, but the approach produces end-to-end verified C code that largely works.
AI-written summary · about
chapters (11)
- 0:00Compositional verification intro
- 1:23Search structure templates core
- 3:30Template approach in practice
- 7:23Logically atomic specs
- 12:02Correctness proofs for CRUD
- 13:25Give up concurrency challenges
- 16:34Deletion complicates separation
- 19:01Proof effort summary
- 20:26VST template reimplementation
- 21:49Formalizing template decomposition
- 22:52Q&A
related talks
15mVerification of Templated Code in C++
15mGradual Verification of Recursive Heap Data Structures
19mPredictable Verification using Intrinsic Definitions
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
22mA Recipe for Modular Verification of Generic Tree Traversals
27mC4: verified transactional objects
18mPreview: Verification (Correctness)