Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Software & patents
Research results
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:

- 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
Software & patents
The C++ Bulk Synchronous Parallelism Library

A prototype to automate semantic mappings between taxonomies

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