Gappa

(Génération Automatique de Preuves de Propriétés Arithmétiques)

Gappa is a tool intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic. It has been used to write robust floating-point filters for CGAL and it is used to certify elementary functions in CRlibm. While Gappa is intended to be used directly, it can also act as a backend prover for the Why software verification plateform or as an automatic tactic for the Coq proof assistant.

Documentation: HTML and PDF versions. Some papers related to Gappa and formal certification of numerical applications are available on Guillaume Melquiond's webpage.

Latest release: Gappa 1.1.1.

Older stable releases: 1.0.0, 0.18.0, 0.17.1. Other releases are available on the Inria Gforge and Lipforge servers.

Support libraries for Coq: 1.0.0 (Coq 8.4, Gappa 1.0.0), 0.21.1 (Coq 8.4, Gappa 0.18.0), 0.19.0 (Coq 8.3, Gappa 0.17.1).

License: Gappa is governed by the CeCILL license under French law and abiding by the rules of distribution of free software. You can use, modify and/or redistribute the software under the terms of the CeCILL license as circulated by CEA, CNRS, and INRIA at the following URL http://www.cecill.info/. Gappa is also released under the terms of the GNU General Public License. The support libraries are released under the terms of the GNU Lesser General Public License.

Latest News

Gappa 1.1.1 released

Guillaume Melquiond - 2014-03-25 10:25 -

Gappa 1.1.0 released

Guillaume Melquiond - 2014-01-10 14:43 -

Gappa 1.0.0 released

Guillaume Melquiond - 2013-07-19 15:38 -

Gappa Coq library 1.0.0 released

Guillaume Melquiond - 2013-07-19 15:37 -

Gappa Coq library 0.21.1 released

Guillaume Melquiond - 2013-07-03 14:13 -

Gappa Coq library 0.21.0 released

Guillaume Melquiond - 2013-06-25 17:38 -

Gappa 0.18.0 released

Guillaume Melquiond - 2013-06-25 17:35 -

Gappa 0.17.0 released

Guillaume Melquiond - 2013-04-17 13:23 -

Gappa Coq Library 0.19.0 released

Guillaume Melquiond - 2013-04-17 13:23 -

Gappa Coq Library 0.20.0 released

Guillaume Melquiond - 2013-04-17 13:22 -

Gappa 0.17.1 released

Guillaume Melquiond - 2013-04-17 13:22 -

Gappa 0.16.6 released

Guillaume Melquiond - 2013-02-20 16:25 -

Gappa 0.16.5 released

Guillaume Melquiond - 2013-02-17 09:16 -

Gappa 0.16.4 released

Guillaume Melquiond - 2013-02-07 14:14 -

Gappa 0.16.3 released

Guillaume Melquiond - 2013-01-06 16:32 -

Gappa 0.16.2 released

Guillaume Melquiond - 2012-12-21 14:16 -

Gappa 0.16.1 released

Guillaume Melquiond - 2012-06-25 14:57 -

Gappa Coq library 0.18.0 released

Guillaume Melquiond - 2012-01-06 16:24 -

Gappa 0.16.0 released

Guillaume Melquiond - 2012-01-06 15:22 -

Gappa Coq library 0.17.0 released

Guillaume Melquiond - 2011-12-08 16:24 -
Project Summary
Tracker Tracker

 - Bugs(0 open / 1 total)

 - Support(0 open / 0 total)

 - Patches(0 open / 0 total)

 - Feature Requests(0 open / 0 total)


SCM SCM Tree ( 298 commits, 10 adds )
FTP Released Files

 

 


Powered By GForge Collaborative Development Environment