@Article{CHJL2010,
  author = {Chevillard, S. and Harrison, J. and Jolde\c{s}, M. and Lauter, C.},
  title =        {{Efficient and accurate computation of upper bounds of approximation errors}},
  journal = 	 {{Theoretical Computer Science}},
  year =         {2011},
  volume = {412},
  number = {16},
  pages = {1523--1543},
  abstract = { For purposes of actual evaluation, mathematical functions $f$ are
               commonly replaced by approximation polynomials $p$. Examples include
               floating-point implementations of elementary functions, quadrature
               or more theoretical proof work involving transcendental functions.

               Replacing $f$ by $p$ induces a relative error $\epsilon =
               \nicefrac{p}{f} - 1$. In order to ensure the validity of the use of
               $p$ instead of $f$, the maximum error, i.e. the supremum norm
               $\ninf{\epsilon}$ must be safely bounded above.

               Numerical algorithms for supremum norms are efficient but cannot
               offer the required safety. Previous validated approaches often
               require tedious manual intervention. If they are automated, they
               have several drawbacks, such as the lack of quality guarantees.

               In this article a novel, automated supremum norm algorithm with
               \emph{a priori} quality is proposed. It focuses on the validation
               step and paves the way for formally certified supremum norms.

               Key elements are the use of intermediate approximation polynomials
               with bounded truncation remainder and a non-negativity test based on
               a Sum-of-squares expression of polynomials.

               The new algorithm was implemented in the tool Sollya. The article
               includes experimental results on real-life examples.
             },
  keywords = { supremum norm, approximation error, Taylor Models, Sum-of-Squares,
               validation, certification, formal proof}
}