To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 08/09/08 - Paris - FR
Vous pouvez vous abonner à nos annonces de séminaires
http://pauillac.inria.fr/seminaires/
S E M I N A I R E
__
/ _` _ / / o /| /| __ __ __ __ _ _
/ ) __) / / / / / /\/| ----- / |/ | / )(_ / / ) ) ) __)
(___/ (_/ (_ (_ / (__/ / | / | (__/ __)(_ (__/ (_/ (_/
I N R I A - Rocquencourt
Amphi Turing du bâtiment 1
Lundi 8 septembre, 10h30
------------
Keiko Nakata
------------
INRIA
===============================================================
Towards less painful verification of the full correctness for C
===============================================================
In this talk I report on my experience in combining an automatic decision
procedure and interactive reasoning to prove the full correctness of a subset
of C programs, or C without goto, based on a separation logic framework. Here
the full correctness means functional correctness plus memory safety,
i.e. execution of the program does not access invalid memory.
We are interested in using an interactive proof assistant, or Coq, as a base
for program verification, since its expressive logic shall be useful to deal
with high-level specifications of sophisticated programs and since its type
system ensures the correctness of the proof which verifies that the program
meets the specification. Our main concern is the potential burden of
verification overhead to the programmer. We expect the programmer to deal with
delicate sub-proofs, but do not want to burden the programmer with tedious
sub-proofs; thus we want to join together interactive and automated
reasoning. In the talk, I report how I addressed the gap between the two world
of the interactive and automated reasoning, by developing a tactic library to
bridge the gap.