## CFML: a Characteristic Formula generator for MLCFML 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.
## Chunked sequences verification demoChunked sequences | | Bootstrapped chunked sequences | |
## Slides from the course given at the MPRI in 2014## Download- The stable source files can be obtained by running:
`svn checkout svn://scm.gforge.inria.fr/svn/cfml/branches/v1 cfml` (does not yet include the chunked seq demo) - 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 bookBatched 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 bookQueues (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 programsDijkstra'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 libraryFormalization 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 | |
## ModelsRealization 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 publicationsCharacteristic 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 |