Quality Software, International Conference on (2007)
Portland, Oregon, USA
Oct. 11, 2007 to Oct. 12, 2007
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/QSIC.2007.1
Sylvain Chevillard , LIP (CNRS/ENS Lyon/INRIA/Univ. Lyon 1), France
Christoph Lauter , LIP (CNRS/ENS Lyon/INRIA/Univ. Lyon 1), France
The high-quality floating-point implementation of use- ful functions f : R R, such as exp, sin, erf requires bounding the error = p-f f of an approximation p with regard to the function f . This involves bounding the infi- nite norm of the error function. Its value must not be underestimated when implementations must be safe. Previous approaches for computing infinite norm are shown to be either unsafe, not sufficiently tight or too te- dious in manual work. We present a safe and self-validating algorithm for auto- matically upper- and lower-bounding infinite norms of er- ror functions. The algorithm is based on enhanced inter- val arithmetic. It can overcome high cancellation and high condition number around points where the error function is defined only by continuous extension. The given algorithm is implemented in a software tool. It can generate a proof of correctness for each instance on which it is run.
C. Lauter and S. Chevillard, "A Certified Infinite Norm for the Implementation of Elementary Functions," 2007 7th International Conference on Quality Software(QSIC), Portland, OR, 2007, pp. 153-160.