Compositional Verification of Concurrent C Programs with Search Structure Templates
Concurrent search structure templates are a technique for separating the verification of a concurrent data structure into concurrency-control and data-structure components, which can then be modularly combined with no additional proof effort. In this paper, we implement the template approach in the Verified Software Toolchain (VST), and use it to prove correctness of C implementations of fine-grained concurrent data structures. This involves translating code, specifications, and proofs to the idiom of C and VST, and gives us another look at the requirements and limitations of the template approach. We encounter several questions about the boundaries between template and data structure, as well as some common data structure operations that cannot naturally be decomposed into templates. Nonetheless, the approach appears promising for modular verification of real-world concurrent data structures.
Tue 16 JanDisplayed time zone: London change
14:00 - 15:30 | |||
14:00 30mTalk | Compositional Verification of Concurrent C Programs with Search Structure Templates CPP Duc-Than Nguyen University of Illinois at Chicago, Lennart Beringer Princeton University, William Mansky University of Illinois Chicago, Shengyi Wang Princeton University, USA Pre-print | ||
14:30 30mTalk | Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logicdistinguished paper CPP Qiyuan Zhao National University of Singapore, George Pîrlea National University of Singapore, Zhendong Ang National University of Singapore, Umang Mathur National University of Singapore, Ilya Sergey National University of Singapore Pre-print | ||
15:00 30mTalk | Unification for Subformula Linking under Quantifiers CPP Pre-print |