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.
- 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
Signatures from Okasaki's book
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)|
|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|
|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|
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