Vers un système de contraintes pour l’analyse des erreurs de précision des calculs sur les flottants⇤

Floating-point computations induce errors linked to the rounding operations required to close the set of floating-point numbers. These errors, which are symptomatic of the distance between the computations over the floats and the computation over the real numbers, are at the origin of many problems, such as the precision or the stability of floating-point computations. They are the subject of numerous works which are based on an overestimation of actual errors. These approaches allow an estimate of the error, an estimate that can be refined by splitting the search space into subdomains, but they do not, strictly speaking, make it possible to reason about ⇤Ces travaux ont été partiellement supportés par l’ANR COVERIF (ANR-15-CE25-0002). †Papier doctorant : Remy Garcia1 est auteur principal. these errors and, for example, to produce input values that excercise a given error. In order to overcome this lack and to enrich the possibilities of analysis of these errors, we introduce in a solver for constraints over the floats, a domain dual to that of the values, the domain of the errors. This domain is associated with each of the variables of the problem. We also introduce the projection functions that allow the filtering of these domains as well as the mechanisms required for the analysis of these errors.