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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixed points. Principles of Programming Languages 4, pages 238–252, 1977.
D. Goldberg. What every computer scientist should know about floating-point arithmetic. ACM Computing Surveys, 23(1), 1991.
E. Goubault. Static analyses of the precision of floating-point operations. In SAS’01, LNCS. Springer-Verlag, 2001.
E. Goubault, D. Guilbaud, A. Pacalet, B. Starynkévitch, and F. Védrine. A simple abstract interpreter for threat detection and test case generation. In Proceedings of WAPATV’01 (ICSE’01), May 2001.
G. Hanrot, V. Lefevre, F. Rouillier, and P. Zimmermann. The MPFR library. Institut de Recherche en Informatique et Automatique, 2001.
N. D. Jones and S. S. Muchnick. A flexible approach to interprocedural flow analysis and programs with recursive data structures. In Proceedings of the 9th ACM Symposium on Principles of Programming Languages, 1982.
M. Martel. Propagation of rounding errors in finite precision computations: a semantics approach. ESOP, 2002.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goubault, E., Martel, M., Putot, S. (2002). Asserting the Precision of Floating-Point Computations: A Simple Abstract Interpreter. In: Le Métayer, D. (eds) Programming Languages and Systems. ESOP 2002. Lecture Notes in Computer Science, vol 2305. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45927-8_15
Download citation
DOI: https://doi.org/10.1007/3-540-45927-8_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43363-7
Online ISBN: 978-3-540-45927-9
eBook Packages: Springer Book Archive