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 Why3 software verification plateform or as an automatic tactic for the Coq proof assistant.

Documentation: HTML.

Latest release: Gappa 1.4.0.
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.0 (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.