Characteristic Formulae for Mechanized Program Verification

Abstract

This dissertation describes 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 behavior 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 the program satisfies a specification expressed in the style of Separation Logic, with respect to total correctness.

The characteristic formula of a program is automatically generated from its source code alone. In particular, there is no need to annotate the source code with specifications or loop invariants, as such information can be given in interactive proof scripts. One key feature of characteristic formulae is that they are of linear size and that they can be pretty-printed in a way that closely resemble the source code they describe, even though they do not refer to the syntax of the programming language.

Characteristic formulae serve as a basis for a tool, called CFML, that supports the verification of Caml programs using the Coq proof assistant. CFML has been employed to verify about half of the content of Okasaki's book on purely functional data structures, and to verify several imperative data structures such as mutable lists, sparse arrays and union-find. CFML also supports reasoning on higher-order imperative functions, such as functions in CPS form and higher-order iterators.

Paper