Characteristic Formulae for the Verification of Imperative Programs


In previous work, I have introduced a new approach to the verification of purely-functional programs, based on the notion of characteristic formulae. The characteristic formula of a program is a higher-order logic formula that provides a sound and complete description of the semantics of that program. The characteristic formula can be automatically generated from a piece of source code, and it is designed to be easily readable and manipulatable from inside an interactive proof assistant. Characteristic formulae thereby offer an effective way of proving that a program satisfies a specification. In this paper, I describe the generalization of characteristic formulae to an imperative programming language. In this setting, characteristic formulae manipulate specifications expressed in the style of Separation Logic, and they integrate the frame rule, which enables local reasoning. This work is implemented in a tool, called CFML, that supports the verification of imperative Caml programs using the Coq proof assistant. CFML has been employed to formalize nontrivial imperative algorithms, and also to reason about CPS functions, higher-order iterators and higher-order stores.


Arthur Charguéraud
ICFP: International Conference on Functional Programming, September 2011