Gappa - Gappa, a tool for certifying numerical applications


Person in charge : MELQUIOND Guillaume


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.

More information: http://gappa.gforge.inria.fr/

- Licence : CeCILL



Research activities
  Program proof
  Floating-point arithmetic
  Automated Proof, SMT and Applications
  Formalisation and Proof of Numerical Programs

Members
  MELQUIOND Guillaume

Group
  Verification of Algorithms, Languages and Systems

BSP++
The C++ Bulk Synchronous Parallelism Library

TAXOMAP ALIGNMENT
A prototype to automate semantic mappings between taxonomies

FR1155729
Procédé pour l’extinction de routeurs dans un réseau de communications et routeur mettant en œuvre ce procédé