Provably Faithful Evaluation of Polynomials

Sylvie Boldo 1 César Muñoz 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 : We provide sufficient conditions that formally guarantee that the floating-point computation of a polynomial evaluation is faithful. To this end, we develop a formalization of floating-point numbers and rounding modes in the Program Verification System (PVS). Our work is based on a well-known formalization of floating-point arithmetic in the proof assistant Coq, where polynomial evaluation has been already studied. However, thanks to the powerful proof automation provided by PVS, the sufficient conditions proposed in our work are more general than the original ones.
Type de document :
Communication dans un congrès
21st Annual ACM Symposium on Applied Computing, Apr 2006, Dijon, France, 2006
Liste complète des métadonnées


https://hal.inria.fr/inria-00000892
Contributeur : Sylvie Boldo <>
Soumis le : jeudi 1 décembre 2005 - 15:22:13
Dernière modification le : jeudi 9 février 2017 - 15:56:34
Document(s) archivé(s) le : vendredi 2 avril 2010 - 23:18:20

Fichiers

Identifiants

  • HAL Id : inria-00000892, version 1

Collections

Citation

Sylvie Boldo, César Muñoz. Provably Faithful Evaluation of Polynomials. 21st Annual ACM Symposium on Applied Computing, Apr 2006, Dijon, France, 2006. <inria-00000892>

Partager

Métriques

Consultations de
la notice

453

Téléchargements du document

150