POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Tue 16 Jan 2024 14:00 - 14:30 at Kelvin Lecture - Mechanized separation logic Chair(s): Amin Timany

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 Jan

Displayed time zone: London change

14:00 - 15:30
Mechanized separation logicCPP at Kelvin Lecture
Chair(s): Amin Timany Aarhus University
14:00
30m
Talk
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
30m
Talk
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
30m
Talk
Unification for Subformula Linking under Quantifiers
CPP
Ike Mulder Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen
Pre-print