In floating-point (FP) arithmetic, having fully-specified operations is a key-requirement, if one wants portable and predictable numerical software. Since 1985, the four arithmetic operations are specified (they must be correctly rounded: the system must return the FP number nearest the exact result). This is not fully the case for the basic mathematical functions. The same function may return significantly different results depending on the environment. Hence, numerical programs using these functions suffer from various problems: • it is almost impossible to estimate their accuracy; • their portability is difficult to guarantee. The lack of specification is due to a problem called the Table Maker’s Dilemma. To compute f(x) in a given format, where x is a FP number, we first compute an approximation to f(x) and then we round it to the nearest FP number. The problem is: what must the accuracy of the approximation be to ensure that the obtained result is always equal to f(x) rounded to the nearest FP number? To solve that problem, we must locate, for each considered FP format & function, what is the hardest to round (HR) point, i.e., the FP number x such that f (x) is closest to the exact middle of two consecutive FP numbers. The naive way of finding it (evaluating f at each FP number) is by far impractical. This project aims at providing • for the most common formats & functions, tables of HR points, with proofs of their correctness; • open source software that allows one to compute HR points for other functions & formats. Getting these points will allow for very efficient math function libraries, leading the path to a full specification of the usual functions in FP arithmetic, with long-term consequences on the quality and portability of numerical software. The state-of-the art can be summarized as follows: • In 1991, IBM released a library, libultim, now abandoned, that claimed correct rounding in double-precision. Since this was done without knowledge of the HR points, the necessary precision for the intermediate calculation was overestimated, resulting in poor performance; • the Arénaire team (one of the applicants) and the CACAO team of LORIA (Nancy) have designed algorithms, and obtained & published HR points for some functions in double precision. The complexity of their methods is exponential with the number of bits of the format, so that they cannot be applied to formats significantly larger than double precision; • in the last years, using the obtained HR points, Arénaire developed a library, CRLibm , that implements the most common functions in double precision. It offers code where the cost of correct rounding is negligible. These performances led the IEEE-754 revision committee to recommend (yet does not impose) correct rounding for some functions. The new 754-2008 standard for FP arithmetic was adopted in 2008. Our methods cannot be used in large precisions. And yet, IEEE 754-2008 specifies 128-bit binary & decimal formats. Also, the processes that generate our HR cases are based on complex and long calculations that cast some doubt on the correctness on the results. Hence, we need to fully reconsider the methods used to get HR points, and focus on 3 aspects: • large precisions: we must get new algorithms for dealing with precisions larger than double. ; • formal proof: we must provide formal proofs of the critical parts of our methods. • aggressive computing: the methods we have designed so far require weeks of computation on hundreds of PCs. Even if we design faster algorithms, to deal with larger formats we must consider various ways of massively parallelizing them. We aim at getting practical results: tables of HR points, programs for getting them, formal proofs of their correctness, with as a consequence faster and better mathematical function programs.