Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Logiciels et brevets
Production scientifique
Logiciel Gappa
Gappa - Outil Gappa de certification de programmes numériques
Date de dernière version : 09 janvier 2017

Responsable : MELQUIOND Guillaume


Gappa est un outil dédié à la vérification et à la preuve formelle des propriétés de programmes numériques s'appuyant sur de l'arithmétique à virgule flottante ou fixe. Il a été utilisé pour écrire des filtres flottants robustes pour CGAL et pour certifier les fonctions élémentaires de CRlibm. Gappa est conçu pour être utilisé directement, mais il peut aussi être utilisé comme prouveur automatique pour la plateforme de vérification de logiciels Why3 ou comme tactique pour l'assistant de preuve Coq.

Pour en savoir plus: http://gappa.gforge.inria.fr/

Logiciel - Licence : CeCILL



Activités de recherche
  Preuve de programme
  Arithmétique flottante
  Démonstration automatique, SMT et applications
  Formalisation et preuves de programmes numériques

Membres
  MELQUIOND Guillaume

Equipe
  Vérification d'Algorithmes, Langages et Systèmes

Equipe-projet Inria
  Toccata
Logiciels et brevets
BOLDR
Query Intermediate Representation Library

CARNAVAL
Database of RNA Recurrent Interaction Networks

PINT
Static analyzer for dynamics of Automata Networks