Arthur Charguéraud

Characteristic Formulae for the Verification of Imperative Programs

I have developed a new approach to program verification based on characteristic formulae. The characteristic formula of a term is a higher-order logic formula that provides a sound and complete description of the semantics of this term. This formula can be generated automatically from the source code alone; in particular, it does not depend on the specifications or the loop invariants. The characteristic formula is constructed in a compositional way and has a size linear in that of the source code. Moreover, the formula can be pretty-printed in a way that closely resembles the source code, and it can be manipulated using tactics in such a way that the user does not even need to know how characteristic formulae are constructed.

Based on these characteristic formulae, I have built a tool, called CFML, that allows for the verification of imperative Caml programs using the Coq proof assistant. CFML can be used to establish the full functional correctness (including termination) of a program with respect to specifications expressed in higher-order logic. I have used CFML to verify half of the content of Chris Okasaki's book on purely functional data structures. I have also verified imperative code such as Dijkstra's shortest path algorithms or the Union-Find data structure. Moreover, I have demonstrated the ability of characteristic formulae to support reasoning on code combining higher-order functions and side-effects, such as functions with local state, functions stored in the store, functions in CPS form, and higher-order iterators on mutable data structures.

Further information and sample proofs can be found on my webpage: http://arthur.chargueraud.org