CFML: Characteristic Formulae for MLCFML 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.0Download of CFML 1.0
Related publicationsArmaë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 Arthur Charguéraud PhD thesis, December 2010 Program verification using characteristic formulaeIn 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 postcondition). This characteristic formula satisfies the following property:
The concept of characteristic formulaThe 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 HennessyMilner'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 lambdacalculi 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 higherorder logic, associated with a prettyprinter, and including support for local reasoning. It is useful to understand what the characteristic formula approach is not:
