Computing a Correct and Tight Rounding Error Bound Using Rounding-to-Nearest

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 epsilon vertical bar x vertical bar or epsilon vertical bar phi(x)vertical bar. 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.