(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 Why3 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.3.5.

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

Support libraries for Coq: 1.4.2 (Coq ≥ 8.8, Gappa ≥ 1.3.2, Flocq ≥ 3.0), 1.4.1 (Coq 8.7 to 8.9, Gappa ≥ 1.3.2, Flocq ≥ 3.0), 1.3.4 (Coq 8.4 to 8.8, Gappa ≥ 1.3.1, Flocq 2.5 & 2.6), 1.2.1 (Coq 8.4 & 8.5, Gappa 1.2.2, Flocq 2.5 & 2.6), 1.1.0 (Coq 8.4, Gappa 1.2.2, Flocq 2.4), 1.0.0 (Coq 8.4, Gappa 1.0.0 & 1.1.2).

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