Static Analysis of the Numerical Stability of Loops

  • Matthieu Martel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2477)


We introduce a relational static analysis to determine the stability of the numerical errors arising inside a loop in which floating-point computations are carried out. This analysis is based on a stability test for non-linear functions and on a precise semantics for floating-point numbers that computes the propagation of the errors made at each operation. A major advantage of this approach is that higher-order error terms are not neglected. We introduce two algorithms for the analysis. The first one, less complex, only determines the global stability of the loop. The second algorithm determines which particular operation makes a loop unstable. Both algorithms have been implemented and we present some experimental results.


Abstract Interpretation Numerical Precision Relational Analysis Semantics of Floating-point Numbers 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    K. T. Alligood, T. D. Sauer, and J. A. Yorke. Chaos, an Introduction to Dynamical Systems. Springer-Verlag, 1996.Google Scholar
  2. 2.
    ANSI/IEEE. IEEE Standard for Binary Floating-point Arithmetic, std 754-1985 edition, 1985.Google Scholar
  3. 3.
    M. F. Barnsley. Fractals Everywhere, Second Edition. Academic Press, 1993.Google Scholar
  4. 4.
    A. F. Beardon. Iteration of Rational Functions. Number 132 in Graduate Texts in Mathematics. Springer-Verlag, 1991.Google Scholar
  5. 5.
    F. Chatelin. Valeurs propres des matrices. Masson, 1988.Google Scholar
  6. 6.
    P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Symbolic Computation, 2(4):511–547, 1992.zbMATHMathSciNetGoogle Scholar
  7. 7.
    D. Goldberg. What every computer scientist should know about floating-point arithmetic. ACM Computing Surveys, 23(1), 1991.Google Scholar
  8. 8.
    G. H. Golub and C. F. Van Loan. Matrix Computations. The Johns Hopkins University Press, 2d edition, 1990.Google Scholar
  9. 9.
    E. Goubault. Static analyses of the precision of floating-point operations. In Static Analysis Symposium, SAS’01, number 2126 in Lecture Notes in Computer Science. Springer-Verlag, 2001.Google Scholar
  10. 10.
    E. Goubault, M. Martel, and S. Putot. Asserting the precision of floating-point computations: a simple abstract interpreter. In European Symposium on Programming, ESOP’02, number 2305 in Lecture Notes in Computer Science. Springer-Verlag, 2002.Google Scholar
  11. 11.
    D. Knuth. The Art of Computer Programming-Seminumerical Algorithms. Addison Wesley, 1973.Google Scholar
  12. 12.
    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.Google Scholar
  13. 13.
    M. Martel. Propagation of roundoff errors in finite precision computations: a semantics approach. In European Symposium on Programming, ESOP’02, number 2305 in Lecture Notes in Computer Science. Springer-Verlag, 2002.Google Scholar
  14. 14.
    F. C. Moon. Chaotic and Fractal Dynamics. Wiley-Interscience, 1992.Google Scholar
  15. 15.
    W. H. Press, S. A. Teukolsky, W. T. Vetterling, and B. P. Flannery. Numerical Recipes in C Cambridge University Press, 1992.Google Scholar
  16. 16.
    J. Vignes. A survey of the CESTAC method. In Proceedings of Real Numbers and Computer Conference, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Matthieu Martel
    • 1
  1. 1.CEA - Recherche TechnologiqueLIST-DTSI-SLAGif-Sur-YvetteFrance

Personalised recommendations