HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 metadata

Cited literature [28 references]  Display  Hide  Download

Contributor : Guillaume Melquiond Connect in order to contact the contributor
Submitted on : Monday, September 14, 2015 - 10:56:09 AM
Last modification on : Wednesday, February 2, 2022 - 3:55:00 PM
Long-term archiving on: : Wednesday, April 26, 2017 - 6:50:53 PM


Files produced by the author(s)



É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⟩



Record views


Files downloads