Wed 18 Jan 2023 13:55 - 14:20 at Avenue34 - Program Logics & Resources Chair(s): Robbert Krebbers

Despite significant progress in the verification of hypervisors, operating systems, and compilers, and in verification tooling, there exists a wide gap between the approaches used in verification projects and conventional development of systems software. We see two main challenges in bringing these closer together: verification handling the complexity of code and semantics of conventional systems software, and verification usability.

We describe an experiment in verification tool design aimed at addressing some aspects of both: we design and implement CN, a separation-logic refinement type system for C systems software, aimed at predictable proof automation, based on a realistic semantics of ISO C. CN reduces refinement typing to decidable propositional logic reasoning, uses first-class resources to support pointer aliasing and pointer arithmetic, features resource inference for iterated separating conjunction, and uses a novel syntactic restriction of ghost variables in specifications to guarantee their successful inference. We implement CN and formalise key aspects of the type system, including a soundness proof of type checking. To demonstrate the usability of CN we use it to verify a substantial component of Google's pKVM hypervisor for Android.

Wed 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

13:30 - 14:45
Program Logics & ResourcesPOPL at Avenue34
Chair(s): Robbert Krebbers Radboud University Nijmegen
13:30
25m
Talk
A High-Level Separation Logic for Heap Space under Garbage Collection
POPL
Alexandre Moine Inria, Arthur Charguéraud Inria; Université de Strasbourg; CNRS; ICube, François Pottier Inria
DOI
13:55
25m
Talk
CN: Verifying Systems C Code with Separation-Logic Refinement Types
POPL
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 Cambridge
DOI
14:20
25m
Talk
Conditional Contextual Refinement
POPL
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-SWS
DOI