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

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 ε|○(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.