Formal Verification of Programs Computing the Floating-Point Average

Sylvie Boldo 1, 2, *
* Auteur correspondant
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : The most well-known feature of floating-point arithmetic is the limited precision, which creates round-off errors and inaccuracies. Another important issue is the limited range, which creates underflow and overflow, even if this topic is dismissed most of the time. This article shows a very simple example: the average of two floating-point numbers. As we want to take exceptional behaviors into account, we cannot use the naive formula (x+y)/2. Based on hints given by Sterbenz, we first write an accurate program and formally prove its properties. An interesting fact is that Sterbenz did not give this program, but only specified it. We prove this specification and include a new property: a precise certified error bound. We also present and formally prove a new algorithm that computes the correct rounding of the average of two floating-point numbers. It is more accurate than the previous one and is correct whatever the inputs.
Type de document :
Communication dans un congrès
Michael Butler; Sylvain Conchon; Fatiha Zaïdi. 17th International Conference on Formal Engineering Methods, Nov 2015, Paris, France. Springer, 9407, pp.17-32, 2015, 〈http://icfem2015.lri.fr/〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01174892
Contributeur : Sylvie Boldo <>
Soumis le : vendredi 10 juillet 2015 - 10:37:12
Dernière modification le : vendredi 27 avril 2018 - 14:40:07
Document(s) archivé(s) le : lundi 12 octobre 2015 - 11:30:34

Fichier

article.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01174892, version 1

Citation

Sylvie Boldo. Formal Verification of Programs Computing the Floating-Point Average. Michael Butler; Sylvain Conchon; Fatiha Zaïdi. 17th International Conference on Formal Engineering Methods, Nov 2015, Paris, France. Springer, 9407, pp.17-32, 2015, 〈http://icfem2015.lri.fr/〉. 〈hal-01174892〉

Partager

Métriques

Consultations de la notice

380

Téléchargements de fichiers

437