Bibtex de la publication

@Article{ MaMe2016.1,
author = {Martin-Dorel, Erik and Melquiond, Guillaume},
title = "{Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq}",
journal = {Journal of Automated Reasoning},
publisher = {Springer-Verlag},
address = {},
year = {2016},
month = {octobre},
volume = {57},
number = {3},
pages = {187--217},
language = {anglais},
URL = {,%20 -},
keywords = {Interval arithmetic, Formal proof, Decision procedure, Coq proof assistant, Floating-point arithmetic, Nonlinear arithmetic},
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.}