CFML - CFML
Date of the last release: 01 January 2014

Person in charge : CHARGUERAUD Arthur


CFML is a tool that can be used to verify Caml programs using the Coq proof assistant. It is based on Characteristic Formulae, which have been developed in Charguéraud's 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), and a Coq library that provides tactics for manipulating characteristic formulae interactively.

A collection of algorithms and data structures, some purely functional and other using imperative code, have been verified using CFML.

More information: http://arthur.chargueraud.org/softs/cfml/

Software - Licence : LGPL



Research activities
  Verification
  Formalisation of (Specification and Programming) Languages in Proof Assistants
  Deductive Verification of Programs

Members
  CHARGUERAUD Arthur

Group
  Verification of Algorithms, Languages and Systems

Joint Inria project team
  Toccata

CODALAB
Codalab

DNADNA
Deep Neural Architectures for DNA

CARTOLABE
CARTOLABE