Abstract
We introduce a concrete semantics for floating-point operations which describes the propagation of roundoff errors throughout a computation. This semantics is used to assert the correctness of an abstract interpretation which can be straightforwardly derived from it. In our model, every elementary operation introduces a new first order error term, which is later combined with other error terms, yielding higher order error terms. The semantics is parameterized by the maximal order of error to be examined and verifies whether higher order errors actually are negligible. We consider also coarser semantics computing the contribution, to the final error, of the errors due to some intermediate computations.
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
References
F. Chaitin-Chatelin and V. Frayssé. Lectures on Finite Precision Computations. SIAM, 1996.
F. Chaitin-Chatelin and E. Traviesas. Precise, a toolbox for assessing the quality of numerical methods and software. In IMACS World Congress on Scientific Computation, Modelling and Applied Mathematics, 2000.
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.
P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Symbolic Computation, 2(4):511–547, 1992.
M. Daumas and J. M. Muller, editors. Qualité des Calculs sur Ordinateur. Masson, 1997.
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 Static Analysis Symposium, SAS’01, number 2126 in LNCS. Springer-Verlag, 2001.
E. Goubault, M. Martel, and S. Putot. Concrete and abstract semantics of fp operations. Technical Report DRT/LIST/DTSI/SLA/LSL/01-058, CEA, 2001.
E. Goubault, M. Martel, and S. Putot. Asserting the precision of floating-point computations: a simple abstract interpreter. In ESOP’02, 2002.
J. R. Hauser. Handling floating-point exceptions in numeric programs. ACM Transactions on Programming Languages and Systems, 18(2), 1996.
W. Kahan. The improbability of probabilistic error analyses for numerical computations. Technical report, Berkeley University, 1991.
W. Kahan. Lecture notes on the status of IEEE standard 754 for binary floatingpoint arithmetic. Technical report, Berkeley University, 1996.
D. Knuth. The Art of Computer Programming-Seminumerical Algorithms. Addison Wesley, 1973.
P. Langlois and F. Nativel. Improving automatic reduction of round-off errors. In IMACS World Congress on Scientific Computation, Modelling and Applied Mathematics, volume 2, 1997.
V. Lefevre, J.M. Muller, and A. Tisserand. Toward correctly rounded transcendentals. IEEE Transactions on Computers, 47(11), 1998.
M. Pichat and J. Vignes. The numerical study of unstable fixed points in a chaotic dynamical system. In IMACS World Congress on Scientific Computation, Modelling and Applied Mathematics,, volume 2, 1997.
J. Vignes. A survey of the CESTAC method. In Proceedings of Real Numbers and Computer Conference, 1996.
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
Martel, M. (2002). Propagation of Roundoff Errors in Finite Precision Computations: A Semantics Approach. 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_14
Download citation
DOI: https://doi.org/10.1007/3-540-45927-8_14
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