Computing a correct and tight rounding error bound using rounding-to-nearest - Archive ouverte HAL Access content directly
Conference Papers Year : 2016

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

(1)
1

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.
Fichier principal
Vignette du fichier
article.pdf (261.08 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01377152 , version 1 (06-10-2016)

Identifiers

  • HAL Id : hal-01377152 , version 1

Cite

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. ⟨hal-01377152⟩
246 View
412 Download

Share

Gmail Facebook Twitter LinkedIn More