Combining Coq and Gappa for Certifying Floating-Point Programs

Sylvie Boldo 1, 2 Jean-Christophe Filliâtre 1, 2 Guillaume Melquiond 1, 2
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : Formal verification of numerical programs is notoriously difficult. On the one hand, there exist automatic tools specialized in floating-point arithmetic, such as Gappa, but they target very restrictive logics. On the other hand, there are interactive theorem provers based on the LCF approach, such as Coq, that handle a general-purpose logic but that lack proof automation for floating-point properties. To alleviate these issues, we have implemented a mechanism for calling Gappa from a Coq interactive proof. This paper presents this combination and shows on several examples how this approach offers a significant speedup in the process of verifying floating-point programs.
Type de document :
Communication dans un congrès
16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Jul 2009, Grand Bend, Ontario, Canada. 5625, pp.59-74, 2009, 〈10.1007/978-3-642-02614-0_10〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00432726
Contributeur : Sylvie Boldo <>
Soumis le : jeudi 11 décembre 2014 - 11:16:14
Dernière modification le : jeudi 5 avril 2018 - 12:30:09
Document(s) archivé(s) le : jeudi 12 mars 2015 - 10:26:48

Fichier

09-calculemus-article.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond. Combining Coq and Gappa for Certifying Floating-Point Programs. 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Jul 2009, Grand Bend, Ontario, Canada. 5625, pp.59-74, 2009, 〈10.1007/978-3-642-02614-0_10〉. 〈inria-00432726〉

Partager

Métriques

Consultations de la notice

425

Téléchargements de fichiers

128