Abstract

In my thesis, I have developed a new approach to program verification, based on characteristic formulae. The characteristic formula of a program is a higher-order logic formula that describes the behaviour of that program, in the sense that it is sound and complete with respect to the semantics. This formula can be exploited in an interactive theorem prover to establish that a program satisfies a specification expressed in the style of Separation Logic. One key feature of characteristic formulae is that they are of linear size and that they can be pretty-printed just like the source code they describe.

Characteristic formulae serve as a basis for a tool, called CFML , that supports the verification of Caml programs using the Coq proof assistant. I have used this tool to verify about half of the content of Okasaki’s book on purely functional data structures. I have also verified a collection of small but tricky imperative functions, such as higher-order iterators on mutable lists, the in-place list reversal function, the CPS -append function, as well as fixed point combinators. In the talk, I will explain how to construct characteristic formulae and show how CFML works in practice.