Skip to Main content Skip to Navigation
Conference papers

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

Sylvie Boldo 1
1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
LRI - Laboratoire de Recherche en Informatique, Inria Saclay - Ile de France
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.
Complete list of metadata

Cited literature [5 references]  Display  Hide  Download
Contributor : Sylvie Boldo Connect in order to contact the contributor
Submitted on : Thursday, October 6, 2016 - 2:56:16 PM
Last modification on : Thursday, July 8, 2021 - 3:46:34 AM
Long-term archiving on: : Friday, February 3, 2017 - 4:04:52 PM


Files produced by the author(s)


  • HAL Id : hal-01377152, version 1


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⟩



Les métriques sont temporairement indisponibles