Vous pouvez vous abonner à nos annonces de séminaires
http://gallium.inria.fr/seminaires/
S E M I N A I R E
__
/ _` _ / / o
/ ) __) / / / / / /\/|
(___/ (_/ (_ (_ / (__/ / |
I N R I A - Paris
2 rue Simone Iff (ou: 41 rue du Charolais)
Salle Lions 1, bâtiment C
Lundi 29 juillet, 10h30
-------------
Aquinas Hobor
-------------
NUS School of Computing and Yale-NUS College
========================================
Certifying Graph-Manipulating C Programs
via Localizations within Data Structures
========================================
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.