(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.1.
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.3.2 (Coq 8.4 & 8.5 & 8.6, Gappa 1.3.1, Flocq 2.5), 1.2.1 (Coq 8.4 & 8.5, Gappa 1.2.2, Flocq 2.5), 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), 0.21.1 (Coq 8.4, Gappa 0.18.0).
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.