 |
 |
|
|
| inria-00000892, version 1 |
 |
|
|
| Voir la fiche détaillée |  BibTeX EndNote TEI RefWorks |
|
|
|||||||||
| 21st Annual ACM Symposium on Applied Computing (2006) |
|
| 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. |
|
|
|
|
|
| 1 : | PROVAL (INRIA Futurs) |
|
INRIA – Université Paris Sud - Paris XI |
| 2 : | National Institute of Aerospace (NIA) |
|
NIA |
|
|
|
|
|
| Domaine | : | Informatique/Logique en informatiqueInformatique/Analyse numérique |
| inria-00000892, version 1 | |
| http://hal.inria.fr/inria-00000892/fr/ | |
| oai:hal.inria.fr:inria-00000892_v1 | |
| Contributeur : Sylvie Boldo | |
| Soumis le : Jeudi 1 Décembre 2005, 15:22:13 | |
| Dernière modification le : Jeudi 1 Décembre 2005, 16:33:21 | |
