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: http://gappa.gforge.inria.fr/

Software - 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

Joint Inria project team
  Toccata
Software & patents
TOUCHTOKENS
Low-cost Solution for Tangible Interfaces

LODATLAS
Browsing Linked Data Catalogs with LODAtlas

BOLDR
Query Intermediate Representation Library