Lecture Notes in Computer Science, 2002, Volume 2305/2002, 287-306, DOI: 10.1007/3-540-45927-8_15

Asserting the Precision of Floating-Point Computations: A Simple Abstract Interpreter

Eric Goubault, Matthieu Martel and Sylvie Putot

View Related Documents

Abstract

The manipulation of real numbers by computers is approximated by floatingpoint arithmetic, which uses a finite representation of numbers. This implies that a (small in general) rounding error may be committed at each operation. Although this approximation is accurate enough for most applications, there are some cases where results become irrelevant because of the precision lost at some stages of the computation, even when the underlying numerical scheme is stable. In this paper, we present a tool for studying the propagation of rounding errors in floating-point computations, that carries out some ideas proposed in [3], [7]. Its aim is to detect automatically a possible catastrophic loss of precision, and its source. The tool is intended to cope with real industrial problems, and we believe it is specially appropriate for critical instrumentation software. On these numerically quite simple programs, we believe our tool will bring some very helpful information, and allow us to find possible programming errors such as potentially dangerous double/float conversions, or blatant unstabilities or losses of accuracy. The techniques used being those of static analysis, the tool will not compete on numerically intensive codes with a numerician’s study of stability. Neither is it designed for helping to find better numerical schemes. But, it is automatic and in comparison with a study of sensitivity to data, brings about the contribution of rounding errors occuring at every intermediary step of the computation. Moreover, static analyzes are sure (but may be pessimistic) and consider a set of possible executions and not just one, which is the essential requirement a verification tool for critical software must meet.
This work was supported by the RTD project IST-1999-20527 “DAEDALUS” of the European FP5 programme.

Fulltext Preview

Image of the first page of the fulltext document