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.