Advertisement

Automating the Verification of Floating-Point Programs

  • Clément FumexEmail author
  • Claude Marché
  • Yannick Moy
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10712)

Abstract

In the context of deductive program verification, handling floating-point computations is challenging. The level of proof success and proof automation highly depends on the way the floating-point operations are interpreted in the logic supported by back-end provers. We address this challenge by combining multiple techniques to separately prove different parts of the desired properties. We use abstract interpretation to compute numerical bounds of expressions, and we use multiple automated provers, relying on different strategies for representing floating-point computations. One of these strategies is based on the native support for floating-point arithmetic recently added in the SMT-LIB standard. Our approach is implemented in the Why3 environment and its front-end SPARK 2014 for the development of safety-critical Ada programs. It is validated experimentally on several examples originating from industrial use of SPARK 2014.

Notes

Acknowledgements

We would like to thank Guillaume Melquiond for his help with the design of the new Why3 theory for FP arithmetic and with the realization in Coq using Flocq. We also thank Florian Schanda for providing the case study used in this article, Mohamed Iguernlala and Bruno Marre for fruitful exchanges on the use of AE_fpa and COLIBRI as well as the anonymous reviewers for their comments.

References

  1. 1.
    Ayad, A., Marché, C.: Multi-prover verification of floating-point programs. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 127–141. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14203-1_11 CrossRefGoogle Scholar
  2. 2.
    Baird, S., Charlet, A., Moy, Y., Taft, T.S.: CodePeer - beyond bug-finding with static analysis. In: Boulanger, J.-L. (ed.) Static Analysis of Software: The Abstract Interpretation. Wiley, Hoboken (2013)Google Scholar
  3. 3.
    Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Let’s verify this with Why3. Int. J. Softw. Tools Technol. Transfer (STTT) 17(6), 709–727 (2015). http://toccata.lri.fr/gallery/fm2012comp.en.html CrossRefGoogle Scholar
  4. 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. J. Autom. Reason. 50(4), 423–456 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Boldo, S., Filliâtre, J.C.: Formal verification of floating-point programs. In: IEEE International Symposium on Computer Arithmetic, pp. 187–194 (2007)Google Scholar
  6. 6.
    Boldo, S., Marché, C.: Formal verification of numerical programs: from C annotated programs to mechanical proofs. Math. Comput. Sci. 5, 377–393 (2011)CrossRefzbMATHGoogle Scholar
  7. 7.
    Boldo, S., Melquiond, G.: Flocq: A unified library for proving floating-point algorithms in Coq. In: 20th IEEE Symposium on Computer Arithmetic, pp. 243–252 (2011)Google Scholar
  8. 8.
    Brain, M., D’silva, V., Griggio, A., Haller, L., Kroening, D.: Deciding floating-point logic with abstract conflict driven clause learning. Form. Methods Syst. Des. 45(2), 213–245 (2014)CrossRefzbMATHGoogle Scholar
  9. 9.
    Carreño, V., Miner, P.S.: Specification of the IEEE-854 floating-point standard in HOL and PVS. In: International Workshop on Higher-Order Logic Theorem Proving and Its Applications (1995)Google Scholar
  10. 10.
    Chapman, R., Schanda, F.: Are we there yet? 20 years of industrial theorem proving with SPARK. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 17–26. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-08970-6_2 Google Scholar
  11. 11.
    Chihani, Z., Marre, B., Bobot, F., Bardin, S.: Sharpening constraint programming approaches for bit-vector theory. In: Salvagnin, D., Lombardi, M. (eds.) CPAIOR 2017. LNCS, vol. 10335, pp. 3–20. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-59776-8_1 CrossRefGoogle Scholar
  12. 12.
    Conchon, S., Iguernlala, M., Ji, K., Melquiond, G., Fumex, C.: A three-tier strategy for reasoning about floating-point numbers in SMT. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 419–435. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63390-9_22 CrossRefGoogle Scholar
  13. 13.
    Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-33826-7_16 CrossRefGoogle Scholar
  14. 14.
    Daumas, M., Melquiond, G.: Certification of bounds on expressions involving rounded operators. Trans. Math. Softw. 37(1), 1–20 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Daumas, M., Rideau, L., Théry, L.: A generic library for floating-point numbers and its application to exact computing. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 169–184. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-44755-5_13 CrossRefGoogle Scholar
  16. 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).  https://doi.org/10.1007/978-3-642-04570-7_6 CrossRefGoogle Scholar
  17. 17.
    Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-73368-3_21 CrossRefGoogle Scholar
  18. 18.
    Fumex, C., Dross, C., Gerlach, J., Marché, C.: Specification and proof of high-level functional properties of bit-level programs. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 291–306. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-40648-0_22 CrossRefGoogle Scholar
  19. 19.
    Fumex, C., Marché, C., Moy, Y.: Automated verification of floating-point computations in ADA programs. Research report RR-9060, Inria (2017)Google Scholar
  20. 20.
    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).  https://doi.org/10.1007/978-3-642-38088-4_31 CrossRefGoogle Scholar
  21. 21.
    Harrison, J.: Floating point verification in HOL light: the exponential function. Form. Methods Syst. Des. 16(3), 271–305 (2000)CrossRefGoogle Scholar
  22. 22.
    Harrison, J.: Formal verification of floating point trigonometric functions. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 254–270. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-40922-X_14 CrossRefGoogle Scholar
  23. 23.
    Harrison, J.: Floating-point verification. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 529–532. Springer, Heidelberg (2005).  https://doi.org/10.1007/11526841_35 CrossRefGoogle Scholar
  24. 24.
    IEEE standard for floating-point arithmetic (2008). https://dx.doi.org/10.1109/IEEESTD.2008.4610935
  25. 25.
    Kosmatov, N., Marché, C., Moy, Y., Signoles, J.: Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 461–478. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47166-2_32 CrossRefGoogle Scholar
  26. 26.
    Leino, K.R.M., Moskal, M.: Usable auto-active verification. In: Usable Verification Workshop (2010)Google Scholar
  27. 27.
    Marché, C.: Verification of the functional behavior of a floating-point program: an industrial case study. Sci. Comput. Program. 96(3), 279–296 (2014)CrossRefGoogle Scholar
  28. 28.
    Marre, B., Michel, C.: Improving the floating point addition and subtraction constraints. In: Cohen, D. (ed.) CP 2010. LNCS, vol. 6308, pp. 360–367. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15396-9_30 CrossRefGoogle Scholar
  29. 29.
    McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press, Cambridge (2015)CrossRefzbMATHGoogle Scholar
  30. 30.
    Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3–17. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24725-8_2 CrossRefGoogle Scholar
  31. 31.
    Monniaux, D.: The pitfalls of verifying floating-point computations. ACM Trans. Programm. Lang. Syst. 30(3), 12 (2008)CrossRefGoogle Scholar
  32. 32.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24 CrossRefGoogle Scholar
  33. 33.
    Rümmer, P., Wahl, T.: An SMT-LIB theory of binary floating-point arithmetic. In: International Workshop on Satisfiability Modulo Theories (2010)Google Scholar
  34. 34.
    Russino, D.M.: A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor. LMS J. Comput. Math. 1, 148–200 (1998)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Clément Fumex
    • 1
    • 2
    • 3
    Email author
  • Claude Marché
    • 1
    • 2
  • Yannick Moy
    • 3
  1. 1.Inria, Université Paris-SaclayPalaiseauFrance
  2. 2.LRI, CNRS & Univ. Paris-SudOrsayFrance
  3. 3.AdaCoreParisFrance

Personalised recommendations