CFML: Characteristic Formulae for ML

CFML is a tool for the interactive verification of OCaml programs, using Coq and Separation Logic. It leverages the idea of Characteristic Formulae, a concept that I developed during my PhD thesis.
CFML 1.0 is the stable tool, however it will become subsumed in the near future by CFML 2.0.
CFML 2.0 will remove dependencies on generated axioms, and it will provide a more expressive logic and more powerful tactics. The foundations of CFML 2.0 are described in my Separation Logic course.

Download of CFML 2.0

  • The source files can be obtained from:

    git clone git@gitlab.inria.fr:charguer/cfml2.git

  • For installation instruction, read the README file.
  • The developments rely on my Coq library TLC.
  • All the files are distributed under the GNU-LGPL license.

Download of CFML 1.0

  • WARNING: the development of CFML 1.0 will soon be discontinued as soon as CFML 2.0 is ready.
  • The source files can be obtained from:

    git clone https://gitlab.inria.fr/charguer/cfml.git

  • For installation instruction, checkout the README file.
  • The developments rely on my Coq library TLC.
  • All the files are distributed under the GNU-LGPL license.

Related publications

Armaël Guéneau, Arthur Charguéraud, and François Pottier
ESOP: European Symposium on Programming, April 2018
Arthur Charguéraud and François Pottier
JAR: Journal of Automated Reasoning, September 2017
Arthur Charguéraud and François Pottier
ESOP: European Symposium on Programming, April 2017
Arthur Charguéraud
CPP: Certified Programs and Proofs, January 2016
Arthur Charguéraud and François Pottier
ITP: International Conference on Interactive Theorem Proving, August 2015
Arthur Charguéraud
Report, journal version of the ICFP'11 paper, October 2012
Arthur Charguéraud
ICFP: International Conference on Functional Programming, September 2011
Arthur Charguéraud
ICFP: International Conference on Functional Programming, September 2010

Program verification using characteristic formulae

In my thesis, I have developed a new approach to program verification based on the notion of characteristic formula. This approach is implemented in a tool, called CFML, which can be used to establish in Coq the full functional correctness of arbitrarily complex Caml programs.

The characteristic formula of a piece of code is a logical formula that describes the semantics of this code (it is a form of strongest post-condition). This characteristic formula satisfies the following property:

  • it is built compositionally and automatically from the source code alone,
  • it has a size linear in that of the source code,
  • it can be displayed in the logic in a way that closely resembles source code (using Coq notation system),
  • it can be manipulated through a small set of specialized tactics that make it unnecessary to know how the formula is constructed
  • it is not just a sound, but also a complete description of the code semantics, meaning that characteristic formulae do not restrict in any way the ability to reason about the code;
  • it supports modular verification, and it integrates the frame rule, which enables local reasoning.

The concept of characteristic formula

The general concept of characteristic formula is not new: it originates in work on process calculi from the 80's (Park, 1981). In this setting, every syntactic process definition is mapped to a formula of Hennessy-Milner's logic. This mapping is such that two syntactic processes are behaviorally equivalent if and only if their associated formulae are logically equivalent. More recently, these results on process calculi were adapted to lambda-calculi by Honda, Berger and Yoshida, who derived a sound and complete Hoare logic for PCF (2006). I have turned the concept of characteristic formula into an effective approach to program verification my building formulae of linear size, expressed in a standard higher-order logic, associated with a pretty-printer, and including support for local reasoning.

It is useful to understand what the characteristic formula approach is not:

  • it is not a verification condition generator (VCG): the source code needs not be annotated with invariants; instead, invariants are provided in interactive proofs;
  • it is not a deep embedding: there is no inductive data type used to represent code syntax, so we avoid all technical issues related to the representation and manipulation of program syntax;
  • it is not a shallow embedding: Caml functions are not represented as Coq functions, so there is no need to resort to monadic programming for avoiding the mismatch between program functions, which can be partial, and logical functions, which must be total;
  • it is not a dynamic logic: characteristic formulae are not expressed in ad-hoc logic but instead in a standard higher-order logic, making it possible to leverage on existing theorem provers.