< Retour au sommaire

A Reduced Product of Absolute and Relative Error Bounds for Floating-point Analysis

Maxime Jacquemin le

Lieu: salle 1073, bât 862

Floating-point numbers are widely used as a computable equivalent of real numbers. However, because the memory of a computer is finite, and because one wants to compute complex equations in no time, floating-point numbers are an approximation of the real numbers with bundles of trade-offs between accuracy and performance. Because of them, each computation step can produce rounding errors. Those rounding errors are guaranteed by the IEEE-754 standard to be small for standard operations. But even if each step produces just a small error, accumulating them can produce a massive difference between the desired behavior of the program and the actual one. Even worse, because of the counterintuitive design of floating point numbers, and because programmers work with them while reasoning with real numbers, understanding why the program does not behave as expected is really hard. In the last fifteen years, several analyzes have been proposed for the computation of guaranteed error bounds of numerical programs. Most of them focused on computing bounds of the absolute errors of the program variables. However, the rounding errors produced by each operation are bounded by the IEEE-754 standard on the relative errors. This strongly suggests that computing relative error bounds can also play a role in the process of computing tight absolute error bounds. Exploring this path has been the main objective of this work. This presentation is divided in two. The first part will be focused on a simple analyzer we implemented in Frama-C, called Numerors, based on intervals and implementing the idea of a reduced product between absolute and relative errors. We will show that it improves sometimes drastically the precision of the analysis. The second part is focused on a relational extension of Numerors using the zonotope framework. In this more implementation oriented part, we will present some difficulties we had to overcome to integrate this relational domain into Frama-C. Finally, we conclude by presenting promising paths we want to explore to further improve Numerors.