MARTIN-DOREL , Érik

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 traditional tools. In fact, the inherent difficulty of computing such bounds often...

Double rounding is a phenomenon that may occur when different floating- point precisions are available on the same system. Although double rounding is, in general, innocuous, it may change the behavior of some useful small floating-point algorithms. We analyze the potential influence of double rounding on the Fast2Sum and 2Sum algorithms, on...

In order to derive efficient and robust floating-point implementations of a given function f, it is crucial to compute its hardest-to-round points, i.e. the floating-point numbers x such that f(x) is closest to the midpoint of two consecutive floating-point numbers. Depending on the floating-point format one is aiming at, this can be highly...

We present a formalisation, within the COQ proof assistant, of univariate Taylor models. This formalisation being executable, we get a generic library whose correctness has been formally proved and with which one can effectively compute rigorous and sharp approximations of univariate functions composed of usual functions such as 1/x, sqrt(x),...

One of the most common and practical ways of representing a real function on machines is by using a polynomial approximation. It is then important to properly handle the error introduced by such an approximation. The purpose of this work is to offer guaranteed error bounds for a specific kind of rigorous polynomial approximation called Taylor...