CFML: a characteristic formula generator for MLCFML is a tool that can be used to verify Caml programs using the Coq proof assistant. CFML is made of two parts: a generator that produces Coq characteristic formulae from Caml code, and a Coq library that provides tactics for manipulating characteristic formulae. Download- The source files can be obtained by running the command
svn checkout svn://scm.gforge.inria.fr/svn/cfml/branches/v1 - The compilation requires OCaml (version >= 10.1) and Coq (version 8.3pl1 or 8.3pl2).
- 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, List.iter, and List.iter on a list of counterns | | | 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 publicationsCharacteristic 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 |