Fran├žais Anglais
Accueil Annuaire Plan du site
Home > Research results > Software & patents
Research results
Software Gappa
Gappa - Gappa, a tool for certifying numerical applications
Date of the last release: 09 January 2017

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:

Software - Licence : CeCILL

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

  MELQUIOND Guillaume

  Verification of Algorithms, Languages and Systems

Joint Inria project team
Software & patents

Deep Neural Architectures for DNA