(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.
Latest release:
Gappa 1.4.2.
Source code is available on the Inria Gitlab server.
Older stable releases:
1.3.5,
1.2.2,
1.1.2,
1.0.0.
Other releases are available there.
Support libraries for Coq:
1.5.5 (Coq ≥ 8.8),
1.4.1 (Coq 8.7 to 8.9).
If you are managing your Coq libraries using
Opam,
you can install the support library using opam install coq-gappa.
Source code is available on the Inria Gitlab server.
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.