## Towards less painful verification of the full correctness for C

### Keiko Nakata

Institute of Cybernetics

Thursday, 25 September 2008, 14:00

Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

**Abstract**: 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 a 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 worlds of the
interactive and automated reasoning, by developing a tactic library to
bridge the gap.

Tarmo Uustalu

Last update 4.9.2008