A certified infinite norm for the implementation of elementary functions

Abstract : The high-quality floating-point implementation of useful functions f : R -> R, such as exp, sin, erf requires bounding the error eps = (p-f)/f of an approximation p with regard to the function f. This involves bounding the infinite norm ||eps|| 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 tedious in manual work. We present a safe and self-validating algorithm for automatically upper- and lower-bounding infinite norms of error functions. The algorithm is based on enhanced interval 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.
Type de document :
Communication dans un congrès
Aditya Mathur, W. Eric Wong, M. F. Lau. Seventh International Conference on Quality Software, Oct 2007, Portland, United States. IEEE, pp.153 -- 160, 2007
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00119810
Contributeur : Sylvain Chevillard <>
Soumis le : mardi 5 juin 2007 - 13:29:36
Dernière modification le : mardi 24 avril 2018 - 13:52:28
Document(s) archivé(s) le : mardi 21 septembre 2010 - 12:48:24

Identifiants

  • HAL Id : ensl-00119810, version 2

Collections

Citation

Sylvain Chevillard, Christoph Lauter. A certified infinite norm for the implementation of elementary functions. Aditya Mathur, W. Eric Wong, M. F. Lau. Seventh International Conference on Quality Software, Oct 2007, Portland, United States. IEEE, pp.153 -- 160, 2007. 〈ensl-00119810v2〉

Partager

Métriques

Consultations de la notice

1015

Téléchargements de fichiers

197