Much work in formal verification of low-level systems is based on one of two approaches: refinement or separation logic. These two approaches have complementary benefits: refinement supports the use of programs as specifications, as well as transitive composition of proofs, whereas separation logic supports conditional specifications, as well as modular ownership reasoning about shared state. A number of verification frameworks employ these techniques in tandem, but in all such cases the benefits of the two techniques remain separate. For example, in frameworks that use relational separation logic to prove contextual refinement, the relational separation logic judgment does not support transitive composition of proofs, while the contextual refinement judgment does not support conditional specifications.
In this paper, we propose Conditional Contextual Refinement (or CCR, for short), the first verification system to not only combine refinement and separation logic in a single framework but also to truly marry them together into a unified mechanism enjoying all the benefits of refinement and separation logic simultaneously. Specifically, unlike in prior work, CCR’s refinement specifications are both conditional (with separation logic pre- and post-conditions) and transitively composable. We implement CCR in Coq and evaluate its effectiveness on a range of interesting examples.
Wed 18 JanDisplayed time zone: Eastern Time (US & Canada) change
13:30 - 14:45
|A High-Level Separation Logic for Heap Space under Garbage Collection|
Alexandre Moine Inria, Arthur Charguéraud Inria; Université de Strasbourg; CNRS; ICube, François Pottier InriaDOI
|CN: Verifying Systems C Code with Separation-Logic Refinement Types|
Christopher Pulte University of Cambridge, Dhruv C. Makwana University of Cambridge, Thomas Sewell University of Cambridge, Kayvan Memarian University of Cambridge, Peter Sewell University of Cambridge, Neel Krishnaswami University of CambridgeDOI
|Conditional Contextual Refinement|
Youngju Song Seoul National University; MPI-SWS, Minki Cho Seoul National University, Dongjae Lee Seoul National University, Chung-Kil Hur Seoul National University, Michael Sammler MPI-SWS, Derek Dreyer MPI-SWSDOI