Skip to Main content Skip to Navigation
Journal articles

Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq

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.
Complete list of metadatas

Cited literature [28 references]  Display  Hide  Download

https://hal.inria.fr/hal-01086460
Contributor : Guillaume Melquiond <>
Submitted on : Monday, September 14, 2015 - 10:56:09 AM
Last modification on : Thursday, March 26, 2020 - 7:37:00 PM
Document(s) archivé(s) le : Wednesday, April 26, 2017 - 6:50:53 PM

File

article.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

617

Files downloads

1304