- Date : 29/07/2019
- Lieu : Inria de Paris
- Intervenant(s) : Aquinas Hobor
- Organisateur(s) : Equipe Gallium
Certifying Graph-Manipulating C Programs via Localizations within Data Structures
Aquinas Hobor (NUS School of Computing and Yale-NUS College)
We develop powerful and general techniques to mechanically verify realistic programs that manipulate heap-represented graphs and related data structures
with intrinsic sharing. We construct a modular and general setup for reasoning about abstract mathematical graphs and use separation logic to define how such abstract graphs are represented concretely in the heap. We upgrade Hobor and Villard's theory of ramification to support existential quantifiers in postconditions and to smoothly handle modified program variables. We demonstrate the generality and power of our techniques by integrating them into the Verified Software Toolchain and certifying the correctness of six graph-manipulating programs written in CompCert C, including a 400-line generational garbage collector for the CertiCoq project.
While doing so, we identify two places where the semantics of C is too weak to define generational garbage collectors of the sort used in the OCaml runtime. Our proofs are entirely machine-checked in Coq.