Computing a correct and tight rounding error bound using rounding-to-nearest

Sylvie Boldo 1
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : When a floating-point computation is done, it is most of the time incorrect. The rounding error can be bounded by folklore formulas, such as ε|x| or ε| o (x)|. This gets more complicated when underflow is taken into account as an absolute term must be considered. Now, let us compute this error bound in practice. A common method is to use a directed rounding in order to be sure to get an over-approximation of this error bound. This article describes an algorithm that computes a correct bound using only rounding to nearest, therefore without requiring a costly change of the rounding mode. This is formally proved using the Coq formal proof assistant to increase the trust in this algorithm.
Type de document :
Communication dans un congrès
9th International Workshop on Numerical Software Verification, Jul 2016, Toronto, Canada. 2016
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01377152
Contributeur : Sylvie Boldo <>
Soumis le : jeudi 6 octobre 2016 - 14:56:16
Dernière modification le : jeudi 11 janvier 2018 - 02:01:56
Document(s) archivé(s) le : vendredi 3 février 2017 - 16:04:52

Fichier

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

Identifiants

  • HAL Id : hal-01377152, version 1

Citation

Sylvie Boldo. Computing a correct and tight rounding error bound using rounding-to-nearest. 9th International Workshop on Numerical Software Verification, Jul 2016, Toronto, Canada. 2016. 〈hal-01377152〉

Partager

Métriques

Consultations de la notice

225

Téléchargements de fichiers

83