This program is tentative and subject to change.

Fri 21 Jan 2022 15:30 - 15:55 at Salon I - Verification 1 Chair(s): Lennart Beringer

Systems code often requires fine-grained control over memory layout and pointers, expressed using low-level (\emph{e.g.}, bitwise) operations on pointer values. Since these operations go beyond what basic pointer arithmetic in C allows, they are performed with the help of \emph{integer-pointer casts}. Prior work has explored increasingly realistic memory object models for C that account for the desired semantics of integer-pointer casts while also being sound w.r.t. compiler optimisations, culminating in PNVI, the preferred memory object model in ongoing discussions within the ISO WG14 C standards committee. However, its complexity makes it an unappealing target for verification, and there exist no tools for verifying C programs under PNVI.

In this paper, we introduce VIP, a new memory object model aimed at supporting C verification. VIP sidesteps the complexities of PNVI with a simple but effective idea: a new construct that lets programmers express the intended provenances of integer-pointer casts explicitly. At the same time, we prove VIP compatible with PNVI, thus enabling verification on top of VIP to benefit from PNVI’s validation with respect to practice. In particular, we build a verification tool, RefinedC-VIP, for verifying programs under VIP semantics. As the name suggests, RefinedC-VIP extends the recently developed RefinedC tool, which is automated yet also produces foundational proofs in Coq. We evaluate RefinedC-VIP on a range of systems-code idioms, as well as validating VIP’s expressiveness via an implementation extending the Cerberus C semantics.

This program is tentative and subject to change.

Fri 21 Jan

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

15:05 - 16:20
Verification 1POPL at Salon I
Chair(s): Lennart Beringer Princeton University
15:05
25m
Research paper
Certifying Derivation of State Machines from CoroutinesInPerson
POPL
Mirai Ikebuchi National Institute of Informatics, Japan, Andres Erbsen MIT, Adam Chlipala Massachusetts Institute of Technology
15:30
25m
Research paper
VIP: Verifying Real-World C Idioms with Integer-Pointer CastsRemote
POPL
Rodolphe Lepigre MPI-SWS, Michael Sammler MPI-SWS, Kayvan Memarian University of Cambridge, Robbert Krebbers Radboud University Nijmegen, Derek Dreyer MPI-SWS, Peter Sewell University of Cambridge
15:55
25m
Research paper
Verified Compilation of C Programs with a Nominal Memory ModelRemote
POPL
Yuting Wang John Hopcroft Center for Computer Science - Shanghai Jiao Tong University, Ling Zhang John Hopcroft Center for Computer Science - Shanghai Jiao Tong University, Zhong Shao Yale University, Jérémie Koenig Yale University
Hide past events