Rigorous Enclosure of Round-Off Errors in Floating-Point Computations.

Efficient tools for error analysis of programs with floating-point computations are available. Most of them provide an over-approximation of the floating-point errors. The point is that these approximations are often too coarse to evaluate the effective impact of the error on the behaviour of a program. Some of these tools compute an under-approximation of the maximal error. But, these under-approximations are either not rigorous or not reachable. In this paper, we introduce a new approach to rigorously enclose the maximal error by means of an over-approximation of the error and an under-approximation computed by means of rational arithmetic. Moreover, our system, called FErA, provides input values that exercise the under-approximations. We outline the advantages and limits of our framework and compare our approach with state-of-the-art methods for over-approximating errors as well as the ones computing under-approximation of the maximal error. Preliminary experiments on standard benchmarks are promising. FErA not only computes good error bounds on most benchmarks but also provides an effective lower bound on the maximal error.