RangeLab: A Static-Analyzer to Bound the Accuracy of Finite-Precision Computations

This article introduces Range Lab, a simple tool to validate the accuracy of floating-point or fixed-point computations. Given intervals for the inputs, Range Lab computes the range of the outputs of simple functions with conditionals and loops as well as a range for the round off errors arising during the computation. Hence the user not only obtains the range of the result of the computation in the computer arithmetic but also a bound on the difference between the computer result and the result in infinite precision. Range Lab is based on static analysis by abstract interpretation and, in this article, we describe the techniques implemented in the tool. In particular, Range Lab uses a hybrid numerical-formal evaluation technique used to limit the wrapping effect in interval computations.