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 Why 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 0.12.3.
Older stable releases:
0.11.3,
0.10.0.
Other releases are available on the
Lipforge server.
Support libraries:
Coq support library 0.13.
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.
|
Tracker
Released Files
