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.