Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq

Érik Martin-Dorel 1 Guillaume Melquiond 2, 3
3 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 verification of floating-point mathematical libraries requires computing numerical bounds on approximation errors. Due to the tightness of these bounds and the peculiar structure of approximation errors, such a verification is out of the reach of generic tools such as computer algebra systems. In fact, the inherent difficulty of computing such bounds often mandates a formal proof of them. In this paper, we present a tactic for the Coq proof assistant that is designed to automatically and formally prove bounds on univariate expressions. It is based on a formalization of floating-point and interval arithmetic, associated with an on-the-fly computation of Taylor expansions. All the computations are performed inside Coq's logic, in a reflexive setting. This paper also compares our tactic with various existing tools on a large set of examples.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2016, 57 (3), pp.187-217. 〈10.1007/s10817-015-9350-4〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01086460
Contributeur : Guillaume Melquiond <>
Soumis le : lundi 14 septembre 2015 - 10:56:09
Dernière modification le : mercredi 12 septembre 2018 - 17:46:03
Document(s) archivé(s) le : mercredi 26 avril 2017 - 18:50:53

Fichier

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

Identifiants

Citation

Érik Martin-Dorel, Guillaume Melquiond. Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. Journal of Automated Reasoning, Springer Verlag, 2016, 57 (3), pp.187-217. 〈10.1007/s10817-015-9350-4〉. 〈hal-01086460v2〉

Partager

Métriques

Consultations de la notice

410

Téléchargements de fichiers

122