Gappa (Génération Automatique de Preuves de Propriétés Arithmétiques -- automatic proof generation of arithmetic properties) is a tool intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic.
The online documentation is available at:
https://gappa.gitlabpages.inria.fr/
Gappa is free software; you can redistribute it and/or modify it under the terms of the CeCILL Free Software License Agreement (see the COPYING file) or under the terms of the GNU General Public License (see the COPYING.GPL file).