(Génération automatique de preuves de propriétés arithmétiques)
Gappa has moved. The most recent releases can be found at its new home.
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 by 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 0.12.0.
Older stable releases: 0.11.3, 0.10.0, 0.9.0, 0.8.0, 0.7.3. Other releases are available on the Lipforge server.
Support libraries: Coq support library 0.12.
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.