INRIA - Logiciels : Outils de preuve

Logiciel	Plates-formes	Distribution	Licence	Equipe-Projet
CoLoR : Bibliothèque Coq sur la recriture et la terminaison	Linux	téléchargeable	CeCILL	PROTHEO
Coq : un système de manipulation de preuves mathématiques formelles	Unix et Windows	téléchargeable	GPL	LOGICAL
daTac: un logiciel de preuve dans les théories associatives commutatives	Unix	téléchargeable	licence gratuite cdri.lor@inria.fr	CASSIS
Elan : un cadre logique pour prototyper résolveurs de contraintes et processus de déduction	Unix	téléchargeable	licence gratuite elan@loria.fr	PROTHEO
Pcoq : une interface graphique pour Coq	Unix et Windows	téléchargeable	cdri.sop@inria.fr	LEMME
Polychrony-Sigali : système formel pour la vérification et la synthèse de contrôleurs.	Unix	téléchargeable	licence gratuite cdri.ren@inria.fr	ESPRESSO
Rainbow : Certificateur de preuves de terminaison	Linux	téléchargeable	CeCILL	PROTHEO
Timbuk : une bibliothèque pour l'analyse d'atteignabilité dans les systèmes de réécriture et la manipulation d'automates d'arbres	Unix	téléchargeable	LGPL	LANDE

Pour chaque logiciel figurant dans ce tableau, on trouve :

une brève description du logiciel qui renvoie sur la page des auteurs ;
les plates-formes sur lesquelles il peut être installé, en considérant les deux grandes familles de systèmes Unix et Windows. Les précisions d'architectures utiles à une installation effective se trouvent sur la page des auteurs ;
le mode de distribution : téléchargeable, cédérom ;
les conditions d'utilisation : libre ou licence (le chargé des relations industrielles pourra vous préciser les conditions d'acquisition) ;
le projet INRIA dans lequel a été conçu et développé ce logiciel.

Logiciel développé en collaboration avec des partenaires