Skip to main content
SpringerLink
Log in

Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions

  • Conference paper
FM 2015: Formal Methods (FM 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9109))

Included in the following conference series:

Abstract

Rigorous estimation of maximum floating-point round-off errors is an important capability central to many formal verification tools. Unfortunately, available techniques for this task often provide overestimates. Also, there are no available rigorous approaches that handle transcendental functions. We have developed a new approach called Symbolic Taylor Expansions that avoids this difficulty, and implemented a new tool called FPTaylor embodying this approach. Key to our approach is the use of rigorous global optimization, instead of the more familiar interval arithmetic, affine arithmetic, and/or SMT solvers. In addition to providing far tighter upper bounds of round-off error in a vast majority of cases, FPTaylor also emits analysis certificates in the form of HOL Light proofs. We release FPTaylor along with our benchmarks for evaluation.

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. Alliot, J.M., Durand, N., Gianazza, D., Gotteland, J.B.: Implementing an interval computation library for OCaml on x86/amd64 architectures (short paper). In: ICFP 2012. ACM (2012)

    Google Scholar 

  2. Barr, E.T., Vo, T., Le, V., Su, Z.: Automatic Detection of Floating-point Exceptions. In: POPL 2013, pp. 549–560. ACM, New York (2013)

    Google Scholar 

  3. Bingham, J., Leslie-Hurd, J.: Verifying Relative Error Bounds Using Symbolic Simulation. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 277–292. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  4. Boldo, S., Clément, F., Filliâtre, J.C., Mayero, M., Melquiond, G., Weis, P.: Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program. Journal of Automated Reasoning 50(4), 423–456 (2013)

    Article  MATH  MathSciNet  Google Scholar 

  5. Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: FMCAD 2009, pp. 69–76 (2009)

    Google Scholar 

  6. Chen, L., Miné, A., Cousot, P.: A Sound Floating-Point Polyhedra Abstract Domain. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 3–18. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  7. Chiang, W.F., Gopalakrishnan, G., Rakamarić, Z., Solovyev, A.: Efficient Search for Inputs Causing High Floating-point Errors. In: PPoPP 2014, pp. 43–52. ACM, New York (2014)

    Google Scholar 

  8. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT Solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013)

    Google Scholar 

  9. The Coq Proof Assistant, http://coq.inria.fr/

  10. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTREÉ Analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Cousot, P., Cousot, R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: POPL 1977, pp. 238–252. ACM, New York (1977)

    Google Scholar 

  12. Daramy, C., Defour, D., de Dinechin, F., Muller, J.M.: CR-LIBM: a correctly rounded elementary function library. Proc. SPIE 5205, 458–464 (2003)

    Google Scholar 

  13. Darulova, E., Kuncak, V.: Trustworthy Numerical Computation in Scala. In: OOPSLA 2011, pp. 325–344. ACM, New York (2011)

    Google Scholar 

  14. Darulova, E., Kuncak, V.: Sound Compilation of Reals. In: POPL 2014, pp. 235–248. ACM, New York (2014)

    Google Scholar 

  15. Daumas, M., Melquiond, G.: Certification of Bounds on Expressions Involving Rounded Operators. ACM Trans. Math. Softw. 37(1), 2:1–2:20 (2010)

    Google Scholar 

  16. Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., Védrine, F.: Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 53–69. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  17. Fousse, L., Hanrot, G., Lefèvre, V., Pélissier, P., Zimmermann, P.: MPFR: A Multiple-precision Binary Floating-point Library with Correct Rounding. ACM Trans. Math. Softw. 33(2) (2007)

    Google Scholar 

  18. Frama-C Software Analyzers, http://frama-c.com/

  19. Gáti, A.: Miller Analyzer for Matlab: A Matlab Package for Automatic Roundoff Analysis. Computing and Informatics 31(4), 713– (2012)

    Google Scholar 

  20. Giannakopoulou, D., Howar, F., Isberner, M., Lauderdale, T., Rakamarić, Z., Raman, V.: Taming Test Inputs for Separation Assurance. In: ASE 2014, pp. 373–384. ACM, New York (2014)

    Google Scholar 

  21. Goodloe, A.E., Muñoz, C., Kirchner, F., Correnson, L.: Verification of Numerical Programs: From Real Numbers to Floating Point Numbers. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 441–446. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  22. Goualard, F.: How Do You Compute the Midpoint of an Interval? ACM Trans. Math. Softw., 40(2) 11:1–11:25 (2014)

    Google Scholar 

  23. Goubault, E., Putot, S.: Static Analysis of Finite Precision Computations. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 232–247. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  24. Haller, L., Griggio, A., Brain, M., Kroening, D.: Deciding floating-point logic with systematic abstraction. In: FMCAD 2012, pp. 131–140 (2012)

    Google Scholar 

  25. Harrison, J.V.: Formal Verification of Floating Point Trigonometric Functions. In: Hunt Jr., W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 217–233. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  26. Harrison, J.: Floating-Point Verification Using Theorem Proving. In: Bernardo, M., Cimatti, A. (eds.) SFM 2006. LNCS, vol. 3965, pp. 211–242. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  27. Harrison, J.: HOL Light: An Overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  28. IEEE Standard for Floating-point Arithmetic. IEEE Std 754-2008, pp. 1–70 (2008)

    Google Scholar 

  29. Johnson, S.G.: The NLopt nonlinear-optimization package, http://ab-initio.mit.edu/nlopt

  30. Kearfott, R.B.: GlobSol User Guide. Optimization Methods Software 24(4-5), 687–708 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  31. Lebbah, Y.: ICOS: A Branch and Bound Based Solver for Rigorous Global Optimization. Optimization Methods Software 24(4-5), 709–726 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  32. Leeser, M., Mukherjee, S., Ramachandran, J., Wahl, T.: Make it real: Effective floating-point reasoning via exact arithmetic. In: DATE 2014, pp. 1–4 (2014)

    Google Scholar 

  33. Linderman, M.D., Ho, M., Dill, D.L., Meng, T.H., Nolan, G.P.: Towards Program Optimization Through Automated Analysis of Numerical Precision. In: CGO 2010, pp. 230–237. ACM, New York (2010)

    Google Scholar 

  34. Martel, M.: Semantics of roundoff error propagation in finite precision calculations. Higher-Order and Symbolic Computation 19(1), 7–30 (2006)

    Article  MATH  Google Scholar 

  35. Martel, M.: Program Transformation for Numerical Precision. In: PEPM 2009, pp. 101–110. ACM, New York (2009)

    Google Scholar 

  36. Martel, M.: RangeLab: A Static-Analyzer to Bound the Accuracy of Finite-Precision Computations. In: SYNASC 2011, pp. 118–122. IEEE Computer Society, Washington, DC (2011)

    Google Scholar 

  37. Maxima: Maxima, a Computer Algebra System. Version 5.30.0 (2013), http://maxima.sourceforge.net/

  38. Melquiond, G.: Floating-point arithmetic in the Coq system. Information and Computation 216(0), 14–23 (2012)

    Article  MATH  MathSciNet  Google Scholar 

  39. Mikusinski, P., Taylor, M.: An Introduction to Multivariable Analysis from Vector to Manifold. Birkhäuser Boston (2002)

    Google Scholar 

  40. Miller, W.: Software for Roundoff Analysis. ACM Trans. Math. Softw. 1(2), 108–128 (1975)

    Article  MATH  Google Scholar 

  41. Moore, R.: Interval analysis. Prentice-Hall series in automatic computation, Prentice-Hall (1966)

    Google Scholar 

  42. de Moura, L., Bjørner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  43. Mutrie, M.P.W., Bartels, R.H., Char, B.W.: An Approach for Floating-point Error Analysis Using Computer Algebra. In: ISSAC 1992, pp. 284–293. ACM, New York (1992)

    Google Scholar 

  44. Neumaier, A.: Taylor Forms - Use and Limits. Reliable Computing 2003, 9–43 (2002)

    MathSciNet  Google Scholar 

  45. Neumaier, A.: Complete search in continuous global optimization and constraint satisfaction. Acta Numerica 13, 271–369 (2004)

    Article  MathSciNet  Google Scholar 

  46. OpenOpt: universal numerical optimization package, http://openopt.org

  47. Paganelli, G., Ahrendt, W.: Verifying (In-)Stability in Floating-Point Programs by Increasing Precision, Using SMT Solving. In: SYNASC, 2013, pp. 209–216 (2013)

    Google Scholar 

  48. Panchekha, P., Sanchez-Stern, A., Wilcox, J.R., Tatlock, Z.: Automatically Improving Accuracy for Floating Point Expressions. In: PLDI 2015. ACM (2015)

    Google Scholar 

  49. Ponsini, O., Michel, C., Rueher, M.: Verifying floating-point programs with constraint programming and abstract interpretation techniques. Automated Software Engineering, 1–27 (2014)

    Google Scholar 

  50. Rakamarić, Z., Emmi, M.: SMACK: Decoupling Source Language Details from Verifier Implementations. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 106–113. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  51. Revol, N., Makino, K., Berz, M.: Taylor models and floating-point arithmetic: proof that arithmetic operations are validated in COSY. The Journal of Logic and Algebraic Programming 64(1), 135–154 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  52. Rümmer, P., Wahl, T.: An SMT-LIB Theory of Binary Floating-Point Arithmetic. In: SMT Workshop 2010 (2010)

    Google Scholar 

  53. Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with taylor interval approximations. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 383–397. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  54. Solovyev, A., Jacobsen, C., Rakamarić, Z., Gopalakrishnan, G.: Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions. Tech. Rep. UUCS-15-001, School of Computing, University of Utah (2015)

    Google Scholar 

  55. Stolfi, J., de Figueiredo, L.: An Introduction to Affine Arithmetic. TEMA Tend. Mat. Apl. Comput. 4(3), 297–312 (2003)

    MATH  MathSciNet  Google Scholar 

  56. Stoutemyer, D.R.: Automatic Error Analysis Using Computer Algebraic Manipulation. ACM Trans. Math. Softw. 3(1), 26–43 (1977)

    Article  MATH  MathSciNet  Google Scholar 

  57. NASA World Wind Java SDK, http://worldwind.arc.nasa.gov/java/

Download references

Author information

Authors and Affiliations

  1. School of Computing, University of Utah, Salt Lake City, UT, 84112, USA

    Alexey Solovyev, Charles Jacobsen, Zvonimir Rakamarić & Ganesh Gopalakrishnan

Authors
  1. Alexey Solovyev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Charles Jacobsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Zvonimir Rakamarić
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ganesh Gopalakrishnan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexey Solovyev .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Nikolaj Bjørner

  2. Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands

    Frank de Boer

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Solovyev, A., Jacobsen, C., Rakamarić, Z., Gopalakrishnan, G. (2015). Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions. In: Bjørner, N., de Boer, F. (eds) FM 2015: Formal Methods. FM 2015. Lecture Notes in Computer Science(), vol 9109. Springer, Cham. https://doi.org/10.1007/978-3-319-19249-9_33

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-19249-9_33

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-19248-2

  • Online ISBN: 978-3-319-19249-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation