OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq

Martin-Dorel, Erik and Melquiond, Guillaume Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. (2016) Journal of Automated Reasoning, vol. 57 (n° 3). pp. 187-217. ISSN 0168-7433

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://dx.doi.org/10.1007/s10817-015-9350-4


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.

Item Type:Article
Additional Information:Thanks to Springer editor. The original PDF can be found at: https://link.springer.com/article/10.1007/s10817-015-9350-4
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
French research institutions > Institut National de la Recherche en Informatique et en Automatique - INRIA (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Deposited By: IRIT IRIT
Deposited On:12 Sep 2017 08:20

Repository Staff Only: item control page