Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Logiciels et brevets
Production scientifique
Logiciel CFML
CFML - Program Verification for ML through Characteristic Formula
Date de dernière version : 01 janvier 2014

Responsable : 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.

Pour en savoir plus: http://arthur.chargueraud.org/softs/cfml/

Logiciel - Licence : LGPL



Activités de recherche
  Vérification
  Formalisation de langages (de spécification et de programmation) dans les assistants de preuve
  Vérification déductive de programmes

Membres
  CHARGUERAUD Arthur

Equipe
  Vérification d'Algorithmes, Langages et Systèmes

Equipe-projet Inria
  Toccata
Logiciels et brevets
SMARTIES
The Smarties Input System

PINT
Static analyzer for dynamics of Automata Networks

SAUPODOC
Semantic Annotation Using Population of Ontology and Definition of Classes