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 dépôt : 01 janvier 1970

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
Logiciels et brevets
BSP++
The C++ Bulk Synchronous Parallelism Library

TAXOMAP ALIGNMENT
Un outil d'alignement de taxonomies

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