INRIA - Software : Proof Tools

Software	Platforms	Distribution	License	Project
CoLoR : Coq Library on Rewriting and termination	Linux	downloadable	CeCILL	PROTHEO
Coq : a system of formal mathematical evidence manipulation	Unix and Windows	downloadable	GPL license	LOGICAL
daTac : a proof application in the commutative associative theories	Unix	downloadable	free license Laurent.Vigneron@loria.fr	CASSIS
Elan : a logic framework for prototyping constraints resolvers deduction processes	Unix	downloadable	free license cdri.lor@inria.fr	PROTHEO
Pcoq : a graphical interface for Coq	Unix and Windows	downloadable	cdri.sop@inria.fr	LEMME
Polychrony-Sigali : an associated formal system for formal verification and controller synthesis	Unix	downloadable	free license cdri.ren@inria.fr	ESPRESSO
Rainbow : termination proof certifier	Linux	downloadable	CeCILL	PROTHEO
Timbuk : A library for Reachability over Term Rewriting Systems and Tree Automata Calculations	Unix	downloadable	LGPL	LANDE

For each software application in this table, the following can be found:

a brief description of the software which goes back to the authors' page ;
and the platforms it can be installed on, taking into account the two main system families Unix and Windows; details of seful architecture for effective installation can be found on the authors' page ;
the distribution mode: downloadable or CD ROM ;
the conditions of use: free or license (the industrial relations manager can give you details of acquisition conditions) ;
the INRIA project under which the software was conceived and developed.

Software developed with external partners