Skip to main content
SpringerLink
Log in

Static Analyses of the Precision of Floating-Point Operations

  • Conference paper
  • First Online:
Static Analysis (SAS 2001)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2126))

Included in the following conference series:

Abstract

Computers manipulate approximations of real numbers, called floating-point numbers. The calculations they make are accurate enough for most applications. Unfortunately, in some (catastrophic) situations, the floating-point operations lose so much precision that they quickly become irrelevant. In this article, we review some of the problems one can encounter, focussing on the IEEE754-1985 norm. We give a (sketch of a) semantics of its basic operations then abstract them (in the sense of abstract interpretation) to extract information about the possible loss of precision. The expected application is abstract debugging of software ranging from simple on-board systems (which use more and more on-the-shelf micro-processors with floating-point units) to scientific codes. The abstract analysis is demonstrated on simple examples and compared with related work.

This work was supported by the RTD project IST-1999-20527 “DAEDALUS”. This paper follows a seminar given at Ecole Normale Supérieure in June 1998.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Y. Ameur, P. Cros, J-J. Falcon, and A. Gomez. An application of abstract interpretation to floating-point arithmetic. In Proceedings of the Workshop on Static Analysis, 1992.

    Google Scholar 

  2. A. Arnold. Sysèmes de transitions finis et sémantique des processus communicants. Masson, 1992.

    Google Scholar 

  3. G. A. Baker. Essentials of Padé approximants. Academic Press, New York, 1975.

    MATH  Google Scholar 

  4. J.-D. Boissonat, F. Cazals, F. Da, O. Devillers, S. Pion, F. Rebufat, M. Teillaud, and M. Yvinec. Programming with CGAL: The example of triangulations. In Proceedings of the Conference on Computational Geometry (SCG’ 99), pages 421–422, New York, N.Y., June 13–16 1999. ACM Press.

    Google Scholar 

  5. A. F. Beardon. Iteration of Rational Functions. Graduate Texts in Mathematics. Springer-Verlag, 1991.

    Google Scholar 

  6. J. C. Bajard, D. Michelucci, J. M. Moreau, and J. M. Muller, editors. Real Numbers and Computers-Les Nombres réels et l’Ordinateur, 1995.

    Google Scholar 

  7. F. Bourdoncle. Interprocedural abstract interpretation of block structured languages with nested procedures, aliasing and recursivity. In PLILP’90, volume 456 of LNCS, pages 307–323. Springer-Verlag, 1990.

    Google Scholar 

  8. F. Bourdoncle. Abstract interpretation by dynamic partitioning. Journal of Functional Programming, 2(4):407–435, 1992.

    Article  MathSciNet  Google Scholar 

  9. F. Bourdoncle. Efficient chaotic iteration strategies with widenings. Lecture Notes in Computer Science, 735, 1993.

    Google Scholar 

  10. P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511–547, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  11. P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper. In M. Bruynooghe and M. Wirsing, editors, Proceedings of the International Workshop Programming Language Implementation and Logic Programming, PLILP’ 92,, Leuven, Belgium, 13–17 August 1992, Lecture Notes in Computer Science 631, pages 269–295. Springer-Verlag, Berlin, Germany, 1992.

    Google Scholar 

  12. F. Chaitin-Chatelin. Le calcul sur ordinateur à précision finie, théorie et état de l’art. Technical Report TR/PA/94/05, CERFACS, 1994.

    Google Scholar 

  13. F. Chaitin-Chatelin and V. Frayss. Lectures on Finite Precision Computations. SIAM, 1996.

    Google Scholar 

  14. F. Chaitin-Chatelin and E. Traviesas. Precise, a toolbox for assessing the quality of numerical methods and software. In 16th IMACS World Congress, 2000.

    Google Scholar 

  15. P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 84–97, Tucson, Arizona, 1978. ACM Press, New York, NY.

    Google Scholar 

  16. J. M. Chesneaux. L’Arithmétique Stochastique et le Logiciel C ADN A Habilitation diriger des recherches, Université Pierre et Marie Curie, Paris, France, November 1995.

    Google Scholar 

  17. C. W. Clenshaw. Rational approximations for special functions. In D. J. Evans, editor, Software for Numerical Mathematics. Academic Press, New York, 1974.

    Google Scholar 

  18. J. M. Chesneaux and J. Vignes. Sur la robustesse de la méthode CESTAC. Comptes Rendus de l’Académie des Sciences, Paris, 307(1):855–860, 1988.

    MATH  MathSciNet  Google Scholar 

  19. J. M. Chesneaux and J. Vignes. Les fondements de l’arithmétique stochastique. Comptes-Rendus de l’Académie des Sciences, Paris, 1(315):1435–1440, 1992.

    MathSciNet  Google Scholar 

  20. M. Daumas and J. M. Muller, editors. Qualité des Calculs sur Ordinateur. Masson, 1997.

    Google Scholar 

  21. A. Edalat. Domains for Computation in Mathematics, Physics and Exact Real Arithmetic. Bulletin of Symbolic Logic, 3(4):401–452, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  22. A. Edalat and P. J. Potts. Exact real computer arithmetic. Technical report, Department of Computing Technical Report DOC 97/9, Imperial College, 1997.

    Google Scholar 

  23. A. Edalat and P. Snderhauf. A Domain-theoretic Approach to Real Number Computation. Theoretical Computer Science, 210:73–98, 1998.

    Article  Google Scholar 

  24. 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.

    Google Scholar 

  25. D. I. Good and R. L. London. Computer interval arithmetic: Definition and proof of correct implementation. Journal of the Association for Computing Machinery, 17(4):603–612, October 1970.

    Google Scholar 

  26. D. Goldberg. What every computer-scientist should know about computer arithmetic. Computing Surveys, 1991.

    Google Scholar 

  27. P. Granger. Improving the results of static analyses of programs by local decreasing iterations. Lecture Notes in Computer Science, 652, 1992.

    Google Scholar 

  28. A. Griewank. Evaluating Derivatives, Principles and Techniques of Algorithmic Differentiation. SIAM, 2000.

    Google Scholar 

  29. J. F. Hart, E. W. Cheney, L. Lawson, H. J. Maehly, C.K. Mesztenyi, J. R. Rice, H. G. Thacher, and C. Witzgall. Computer Approximations. Wiley, New York, 1968.

    MATH  Google Scholar 

  30. N. J. Higham. Accuracy and Stability of Numerical Algorithms. SIAM, Philadelphia, 1996.

    MATH  Google Scholar 

  31. W. Kahan. The improbability of probabilistic error analyses for numerical computations. Technical report, University of Berkeley, 1991.

    Google Scholar 

  32. W. Kahan. Lecture notes on the status of IEEE standard 754 for binary floating-point arithmetic. Technical report, Berkeley University, 1996.

    Google Scholar 

  33. M. Karr. Affine relationships between variables of a program. Acta Informatica, (6):133–151, 1976.

    Google Scholar 

  34. W. Krandick and J. R. Johnson. Efficient multiprecision floating point multiplication with optimal directional rounding. In E. E. Swartzlander, M. J. Irwin, and J. Jullien, editors, Proceedings of the 11th IEEE Symposium on Computer Arithmetic, pages 228–233, Windsor, Canada, June 1993. IEEE Computer Society Press, Los Alamitos, CA.

    Chapter  Google Scholar 

  35. S. Kla. Calcul parallèle et en ligne des fonctions arithmétiques. PhD thesis, Ecole Normale Supérieure de Lyon, 46 Allée d’Italie, 69364 Lyon Cedex 07, France, February 1993.

    Google Scholar 

  36. P. Kornerup and D. W. Matula. Finite-precision rational arithmetic: an arithmetic unit. IEEE Transactions on Computers, C-32:378–388, 1983.

    Article  MathSciNet  Google Scholar 

  37. P. Kornerup and D. W. Matula. Finite precision lexicographic continued fraction number systems. In Proceedings of the 7th IEEE Symposium on Computer Arithmetic, Urbana, USA, 1985. IEEE Computer Society Press, Los Alamitos, CA. Reprinted in E. E. Swartzlander, Computer Arithmetic, Vol. 2, IEEE Computer Society Press Tutorial, Los Alamitos, CA, 1990.

    Google Scholar 

  38. P. Kornerup and D. W. Matula. An on-line arithmetic unit for bit-ipelined rational arithmetic. Journal of Parallel and distributed Computing, Special Issue on Parallelism in Computer Arithmetic(5), 1988.

    Google Scholar 

  39. D. Knuth. The Art of Computer Programming, volume 2. Addison Wesley, Reading, MA, 1973.

    Google Scholar 

  40. V. Lefevre, J.M. Muller, and A. Tisserand. Toward correctly rounded transcendentals. IEEE Transactions on Computers, 47(11), 1998.

    Google Scholar 

  41. 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 

  42. M. Martel. Semantics of floating point operations with error understanding. Technical report, CEA, submitted, May 2001.

    Google Scholar 

  43. D. Monniaux. Abstract interpretation of probabilistic semantics. In Seventh International Static Analysis Symposium (SAS’00), number 1824 in Lecture Notes in Computer Science. Springer-Verlag, 2000.

    Google Scholar 

  44. D. Monniaux. An abstract Monte-Carlo method for the analysis of probabilistic programs (extended abstract). In 28th Symposium on Principles of Programming Languages (POPL’ 01). Association for Computer Machinery, 2001.

    Google Scholar 

  45. R. E. Moore. Methods and Applications of Interval Analysis. Society for Industrial and Applied Mathematics, Philadelphia, PA, USA, 1979.

    MATH  Google Scholar 

  46. P. J. Potts and A. Edalat. A new representation of exact real numbers. Electronic Notes in Computer Science, 6, 1998.

    Google Scholar 

  47. P. J. Potts, A. Edalat, and H. M. Escardó. Semantics of exact real arithmetic. In Procs of Logic in Computer Science. IEEE Computer Society Press, 1997.

    Google Scholar 

  48. G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus, 1981.

    Google Scholar 

  49. M. La Porte and J. Vignes. Error analysis in computing. In Information Processing 74 North-Holland, 1974.

    Google Scholar 

  50. N. Regal. Petite analyse en nombres flottants. Technical Report DTA/LETI/DEIN/SLA/99-055, CEA, 1999.

    Google Scholar 

  51. J. E. Robertson and K. S. Trivedi. The status of investigations into computer hardware design based on the use of continued fractions. IEEE Transactions on Computers, C-22:555–560, 1973.

    Google Scholar 

  52. C. W. Schelin. Calculator function approximation. American Mathematical Monthly, 90(5), May 1983.

    Google Scholar 

  53. M. Scott. Fast rounding in multiprecision floating-slash arithmetic. IEEE Transactions on Computers, 38:1049–1052, 1989.

    Article  MATH  Google Scholar 

  54. R. B. Seidensticker. Continued fractions for high-speed and high-accuracy computer arithmetic. In Proceedings of the 6th IEEE Symposium on Com-puter Arithmetic, Aarhus, Denmark, 1983. IEEE Computer Society Press, Los Alamitos, CA.

    Google Scholar 

  55. J. Vignes and R. Alt. An efficient stochastic method for round-off error analysis. In Miranker Willard and Toupin, editors, Accurate Scientific Computations, Lecture notes in Computer Science 235. Springer-Verlag, 1985.

    Google Scholar 

  56. M. Vincius, A. Andrade, J. L. D. Comba, and J. Stolfi. Affine arithmetic. In INTERVAL March 1994.

    Google Scholar 

  57. J. Vignes. New methods for evaluating the validity of mathematical software. Math. Simul. IMACS, 20:227–249, 1978.

    Article  MathSciNet  MATH  Google Scholar 

  58. J. Vignes. Controle et estimation stochastique des arrondis de calcul. AFCET Interfaces, 54:3–10, 1987.

    Google Scholar 

  59. J. Vignes. A stochastic arithmetic for reliable scientific computation. Math. Comp. Simul., 35:233–261, 1993.

    Article  MathSciNet  Google Scholar 

  60. J. Vignes. A survey of the CESTAC method. In Proceedings of Real Numbers and Computer Conference, 1996.

    Google Scholar 

  61. J. E. Vuillemin. Exact real computer arithmetic with continued fractions. IEEE Transactions on Computers, 39(8), 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIST (CEA - Recherche Technologique) DTSI-SLA, CEA, F91191, Gif-sur-Yvette Cedex

    Eric Goubault

Authors
  1. Eric Goubault
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Département d’Informatique, École Normale Supérieure, 45 rue d’Ulm, 75230, Paris Cedex 05, France

    Patrick Cousot

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Goubault, E. (2001). Static Analyses of the Precision of Floating-Point Operations. In: Cousot, P. (eds) Static Analysis. SAS 2001. Lecture Notes in Computer Science, vol 2126. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47764-0_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-47764-0_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42314-0

  • Online ISBN: 978-3-540-47764-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation