CFML: a Characteristic Formula generator for ML

CFML can be used to verify Caml programs using the Coq proof assistant. It is based on Characteristic Formulae which I have developed during my thesis. CFML consists of two parts:
  • a generator that parses Caml code and produces characteristic formulae expressed as Coq axioms (the generator itself is implemented in Caml),
  • a Coq library that provides tactics for manipulating characteristic formulae interactively.

Download

  • The source files can be obtained by running:
    svn checkout svn://scm.gforge.inria.fr/svn/cfml/branches/v1 cfml
  • The compilation requires Coq v8.4 and OCaml (>= 10.1).
  • The developments rely on my Coq library TLC, which comes with CFML.
  • All the files are distributed under the GNU-LGPL license.
  • The documentation contains the details for the installation procedure and an overview of the tactics available.

Data structures from Okasaki's book

Batched queue (page 43)
Bankers queue (page 65)
Physicists queue (page 73)
Real-time queue (page 83)
Implicit queue (page 174)
Bootstrapped queue (page 149)
Hood-Melville queue (page 105)
Leftist heap (page 20)
Pairing heap (page 54)
Lazy pairing heap (page 80)
Splay heap (page 50)
Binominal heap (page 24)
Unbalanced set (page 14)
Red-black set (page 28)
Bottom-up merge sort (page 77)
Catenable lists (page 156)
Binary random-access lists (page 123)

Signatures from Okasaki's book

Queues (page 42)
Double-ended queues (page 45)
Ordered types (page 14)
Finite sets (page 12)
Heaps (page 18)
Sortable collections (page 74)
Random-access lists (page 120)
Catenable lists (page 153)

Verification of imperative programs

Dijkstra's shortest path algorithm
Sparse arrays (from the Vacid challenge)
Mutable list: length, destructive append, cps-append
Counter generator, and call to iter on a list of counters
Union-Find (without path compression nor ranks)
Factorial with recursion, for loop, and while loop
The composition function
The swap function for two references
Landin's knot (recursion through the store)

CFML library

Formalization of heaps and separation logic tactics
Definitions and lemmas related to specification
Notation for displaying formulae and specifications
Specification of primitive functions
Tactics for manipulating characteristic formulae
Bundle exporting all the library

Models

Realization of AppReturns based on the deep embedding of a pure language
Proof of soundness and completness of characteristic formulae for a basic imperative language

Related publications

Characteristic Formulae for the Verification of Imperative Programs
(Journal version of ICFP'11). Submitted, October 2012
Characteristic Formulae for the Verification of Imperative Programs
International Conference on Functional Programming (ICFP), September 2011
Program Verification Through Characteristic Formulae
International Conference on Functional Programming (ICFP), September 2010
Characteristic Formulae for Mechanized Program Verification
PhD thesis, December 2010