Compositional Verification of Concurrent C Programs with Search Structure Templates
Explore a 27-minute conference talk from CPP 2024 that delves into the compositional verification of concurrent C programs using search structure templates. Learn how researchers Duc-Than Nguyen, Lennart Beringer, William Mansky, and Shengyi Wang implement the template approach in the Verified Software Toolchain (VST) to prove the correctness of fine-grained concurrent data structures in C. Discover the challenges and insights gained from translating code, specifications, and proofs to the C and VST idiom, including questions about template and data structure boundaries. Gain understanding of the potential and limitations of this modular verification approach for real-world concurrent data structures. The talk covers topics such as concurrent separation logic, fine-grained locking, Iris, logical atomicity, and interactive theorem proving, providing valuable insights for researchers and practitioners in software verification and concurrent programming.