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 metadatas

Cited literature [5 references]  Display  Hide  Download

https://hal.inria.fr/hal-01377152
Contributor : Sylvie Boldo <>
Submitted on : Thursday, October 6, 2016 - 2:56:16 PM
Last modification on : Monday, December 14, 2020 - 5:24:05 PM
Long-term archiving on: : Friday, February 3, 2017 - 4:04:52 PM

File

article.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01377152, version 1

Collections

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. ⟨hal-01377152⟩

Share

Metrics

Record views

498

Files downloads

567