Advertisement

A Reduced Product of Absolute and Relative Error Bounds for Floating-Point Analysis

  • Maxime JacqueminEmail author
  • Sylvie Putot
  • Franck Védrine
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11002)

Abstract

Rigorous estimation of bounds on errors in finite precision computation has become a key point of many formal verification tools. The primary interest of the use of such tools is generally to obtain worst-case bounds on the absolute errors. However, the natural bound on the elementary error committed by each floating-point arithmetic operation is a bound on the relative error, which suggests that relative error bounds could also play a role in the process of computing tight error estimations. In this work, we introduce a very simple interval-based abstraction, combining absolute and relative error propagations. We demonstrate with a prototype implementation how this simple product allows us in many cases to improve absolute error bounds, and even to often favorably compare with state-of-the art tools, that rely on much more costly relational abstractions or optimization-based estimations.

Notes

Acknowledgments

The work was partially supported by ANR project ANR-15-CE25-0002. We also gratefully acknowledge the help of the anonymous reviewers and Jérôme Féret, in improving the presentation of this work.

References

  1. 1.
    Comba, J.L.D., Stolfi, J.: Affine arithmetic and its applications to computer graphics. In: SEBGRAPI 1993 (1993)Google Scholar
  2. 2.
    Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the Second International Symposium on Programming, pp. 106–130. Dunod, Paris (1976)Google Scholar
  3. 3.
    Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of ISOP 1976, pp. 106–130. Dunod, Paris (1976)Google Scholar
  4. 4.
    Darulova, E., Kuncak, V.: Trustworthy numerical computation in Scala. In: OOPSLA (2011)Google Scholar
  5. 5.
    Darulova, E., Kuncak, V.: Sound compilation of reals. In: POPL 2014, pp. 235–248, New York, NY, USA. ACM (2014)Google Scholar
  6. 6.
    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
  7. 7.
    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).  https://doi.org/10.1007/978-3-642-04570-7_6CrossRefGoogle Scholar
  8. 8.
    Goubault, E.: Static analyses of the precision of floating-point operations. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 234–259. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-47764-0_14CrossRefzbMATHGoogle Scholar
  9. 9.
    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).  https://doi.org/10.1007/978-3-642-18275-4_17CrossRefGoogle Scholar
  10. 10.
    Goubault, E., Putot, S.: Robustness analysis of finite precision implementations. In: APLAS, pp. 50–57 (2013)Google Scholar
  11. 11.
    Izycheva, A., Darulova, E.: On sound relative error bounds for floating-point arithmetic. In: Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017, pp. 15–22 (2017)Google Scholar
  12. 12.
    Magron, V., Constantinides, G., Donaldson, A.: Certified roundoff error bounds using semidefinite programming. SubmittedGoogle Scholar
  13. 13.
    Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to Interval Analysis (2009)Google Scholar
  14. 14.
    Wilcox, J.-R., Panchekha, P., Sanchez-Stern, A., Tatlock, Z.: Automatically improving accuracy for floating point expressions. In: Grove, D., Blackburn, S. (eds.) PLDI 2015, pp. 1–11. ACM (2015)Google Scholar
  15. 15.
    Rump, S.M., Ogita, T., Oishi, S.: Accurate floating-point summation part i: faithful rounding. SIAM J. Sci. Comput. 31(1), 189–224 (2008)Google Scholar
  16. 16.
    Solovyev, A., Jacobsen, C., Rakamarić, Z., Gopalakrishnan, G.: Rigorous estimation of floating-point round-off errors with symbolic taylor expansions. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 532–550. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-19249-9_33CrossRefGoogle Scholar
  17. 17.
    Titolo, L., Feliú, M.A., Moscato, M., Muñoz, C.A.: An abstract interpretation framework for the round-off error analysis of floating-point programs. Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 10747, pp. 516–537. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-73721-8_24CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Maxime Jacquemin
    • 1
    Email author
  • Sylvie Putot
    • 2
  • Franck Védrine
    • 1
  1. 1.CEA, List, Software Reliability and Security Laboratory, PC 174Gif-Sur-YvetteFrance
  2. 2.LIX, CNRS and École PolytechniquePalaiseauFrance

Personalised recommendations