Advertisement

Verifying Floating-Point Algorithms

  • Jean-Michel Muller
  • Nicolas Brunie
  • Florent de Dinechin
  • Claude-Pierre Jeannerod
  • Mioara Joldes
  • Vincent Lefèvre
  • Guillaume Melquiond
  • Nathalie Revol
  • Serge Torres
Chapter

Abstract

While the previous chapters have made clear that it is common practice to verify floating-point algorithms with pen-and-paper proofs, this practice can lead to subtle bugs. Indeed, floating-point arithmetic introduces numerous special cases, and examining all the details would be tedious. As a consequence, the verification process tends to focus on the main parts of the correctness proof, so that it does not grow out of reach.

References

  1. [6]
    B. Akbarpour, A. T. Abdel-Hamid, S. Tahar, and J. Harrison. Verifying a synthesized implementation of IEEE-754 floating-point exponential function using HOL. The Computer Journal, 53(4):465, 2010.CrossRefGoogle Scholar
  2. [31]
    G. Barrett. Formal methods applied to a floating-point system. IEEE Transactions on Software Engineering, 15(5):611–621, 1989.CrossRefGoogle Scholar
  3. [42]
    S. Boldo. Pitfalls of a full floating-point proof: example on the formal proof of the Veltkamp/Dekker algorithms. In 3rd International Joint Conference on Automated Reasoning (IJCAR), volume 4130 of Lecture Notes in Computer Science, pages 52–66, Seattle, WA, USA, 2006.CrossRefGoogle Scholar
  4. [43]
    S. Boldo. Kahan’s algorithm for a correct discriminant computation at last formally proven. IEEE Transactions on Computers, 58(2):220–225, 2009.MathSciNetCrossRefGoogle Scholar
  5. [44]
    S. Boldo. How to compute the area of a triangle: a formal revisit. In 21th IEEE Symposium on Computer Arithmetic (ARITH-21), pages 91–98, Austin, TX, USA, April 2013.Google Scholar
  6. [45]
    S. Boldo. Formal verification of programs computing the floating-point average. In 17th International Conference on Formal Engineering Methods (ICFEM), volume 9407 of Lecture Notes in Computer Science, pages 17–32, Paris, France, November 2015.CrossRefGoogle Scholar
  7. [51]
    S. Boldo, J.-H. Jourdan, X. Leroy, and G. Melquiond. Verified compilation of floating-point computations. Journal of Automated Reasoning, 54(2):135–163, 2015.MathSciNetCrossRefGoogle Scholar
  8. [52]
    S. Boldo and G. Melquiond. Emulation of FMA and correctly rounded sums: proved algorithms using rounding to odd. IEEE Transactions on Computers, 57(4):462–471, 2008.MathSciNetCrossRefGoogle Scholar
  9. [53]
    S. Boldo and G. Melquiond. Flocq: A unified library for proving floating-point algorithms in Coq. In 20th IEEE Symposium on Computer Arithmetic (ARITH-20), pages 243–252, Tübingen, Germany, 2011.Google Scholar
  10. [54]
    S. Boldo and G. Melquiond. Computer Arithmetic and Formal Proofs. ISTE Press – Elsevier, 2017.Google Scholar
  11. [55]
    S. Boldo and J.-M. Muller. Exact and approximated error of the FMA. IEEE Transactions on Computers, 60(2):157–164, 2011.MathSciNetCrossRefGoogle Scholar
  12. [56]
    S. Boldo and C. Muñoz. Provably faithful evaluation of polynomials. In ACM Symposium on Applied Computing, pages 1328–1332, Dijon, France, 2006.Google Scholar
  13. [72]
    N. Brisebarre, M. Joldeş, É. Martin-Dorel, M. Mayero, J.-M. Muller, I. Paşca, L. Rideau, and L. Théry. Rigorous polynomial approximation using Taylor models in Coq. In 4th International Symposium on NASA Formal Methods (NFM), volume 7226 of Lecture Notes in Computer Science, pages 85–99, Norfolk, VA, USA, 2012.Google Scholar
  14. [96]
    S. Chevillard, J. Harrison, M. Joldeş, and C. Lauter. Efficient and accurate computation of upper bounds of approximation errors. Theoretical Computer Science, 412(16):1523–1543, 2011.MathSciNetCrossRefGoogle Scholar
  15. [119]
    M. Cornea, C. Iordache, J. Harrison, and P. Markstein. Integer divide and remainder operations in the IA-64 architecture. In 4th Conference on Real Numbers and Computers (RNC-4), 2000.Google Scholar
  16. [134]
    M. Daumas and G. Melquiond. Certification of bounds on expressions involving rounded operators. Transactions on Mathematical Software, 37(1):1–20, 2010.MathSciNetCrossRefGoogle Scholar
  17. [135]
    M. Daumas, G. Melquiond, and C. Muñoz. Guaranteed proofs using interval arithmetic. In 17th IEEE Symposium on Computer Arithmetic (ARITH-17), pages 188–195, Cape Cod, MA, USA, 2005.Google Scholar
  18. [136]
    M. Daumas, L. Rideau, and L. Théry. A generic library of floating-point numbers and its application to exact computing. In 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), pages 169–184, Edinburgh, Scotland, 2001.Google Scholar
  19. [200]
    S. A. Figueroa. When is double rounding innocuous? ACM SIGNUM Newsletter, 30(3), 1995.Google Scholar
  20. [238]
    J. Harrison. Floating-point verification in HOL light: The exponential function. Technical Report 428, University of Cambridge Computer Laboratory, 1997.Google Scholar
  21. [239]
    J. Harrison. Verifying the accuracy of polynomial approximations in HOL. In 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 1275 of Lecture Notes in Computer Science, pages 137–152, Murray Hill, NJ, USA, 1997.Google Scholar
  22. [240]
    J. Harrison. A machine-checked theory of floating point arithmetic. In 12th International Conference in Theorem Proving in Higher Order Logics (TPHOLs), volume 1690 of Lecture Notes in Computer Science, pages 113–130, Nice, France, September 1999.Google Scholar
  23. [241]
    J. Harrison. Formal verification of floating-point trigonometric functions. In 3rd International Conference on Formal Methods in Computer-Aided Design (FMCAD), number 1954 in Lecture Notes in Computer Science, pages 217–233, Austin, TX, USA, 2000.Google Scholar
  24. [242]
    J. Harrison. Formal verification of IA-64 division algorithms. In 13th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 1869 of Lecture Notes in Computer Science, pages 233–251, 2000.Google Scholar
  25. [243]
    J. Harrison. Floating-point verification using theorem proving. In Formal Methods for Hardware Verification, 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006, volume 3965 of Lecture Notes in Computer Science, pages 211–242, Bertinoro, Italy, 2006.CrossRefGoogle Scholar
  26. [244]
    J. Harrison. Verifying nonlinear real formulas via sums of squares. In 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 4732 of Lecture Notes in Computer Science, pages 102–118, Kaiserslautern, Germany, 2007.Google Scholar
  27. [261]
    J. E. Holm. Floating-Point Arithmetic and Program Correctness Proofs. Ph.D. thesis, Cornell University, 1980.Google Scholar
  28. [285]
    C. Jacobi and C. Berg. Formal verification of the VAMP floating point unit. Formal Methods in System Design, 26(3):227–266, 2005.CrossRefGoogle Scholar
  29. [286]
    C. Jacobsen, A. Solovyev, and G. Gopalakrishnan. A parameterized floating-point formalization in HOL Light. In 7th and 8th International Workshops on Numerical Software Verification (NSV), volume 317 of Electronic Notes in Theoretical Computer Science, pages 101–107, 2015.CrossRefGoogle Scholar
  30. [323]
    R. Kaivola and K. Kohatsu. Proof engineering in the large: formal verification of Pentium®;4 floating-point divider. International Journal on Software Tools for Technology Transfer, 4(3):323–334, 2003.CrossRefGoogle Scholar
  31. [408]
    É. Martin-Dorel and G. Melquiond. Proving tight bounds on univariate expressions with elementary functions in Coq. Journal of Automated Reasoning, 57(3):187–217, 2016.MathSciNetCrossRefGoogle Scholar
  32. [409]
    É. Martin-Dorel, G. Melquiond, and J.-M. Muller. Some issues related to double rounding. BIT Numerical Mathematics, 53(4):897–924, 2013.MathSciNetCrossRefGoogle Scholar
  33. [416]
    G. Melquiond. Proving bounds on real-valued functions with computations. In 4th International Joint Conference on Automated Reasoning (IJCAR), volume 5195 of Lecture Notes in Artificial Intelligence, pages 2–17, 2008.Google Scholar
  34. [417]
    G. Melquiond. Floating-point arithmetic in the Coq system. Information and Computation, 216:14–23, 2012.MathSciNetCrossRefGoogle Scholar
  35. [426]
    J. S. Moore, T. Lynch, and M. Kaufmann. A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating point division algorithm. IEEE Transactions on Computers, 47(9):913–926, 1998.MathSciNetCrossRefGoogle Scholar
  36. [447]
    C. Muñoz and A. Narkawicz. Formalization of Bernstein polynomials and applications to global optimization. Journal of Automated Reasoning, 51(2):151–196, 2013.MathSciNetCrossRefGoogle Scholar
  37. [474]
    J. O’Leary, X. Zhao, R. Gerth, and C.-J. H. Seger. Formally verifying IEEE compliance of floating point hardware. Intel Technology Journal, 3(1), 1999.Google Scholar
  38. [495]
    D. M. Priest. Algorithms for arbitrary precision floating point arithmetic. In 10th IEEE Symposium on Computer Arithmetic (ARITH-10), pages 132–143, June 1991.Google Scholar
  39. [516]
    P. Roux. Innocuous double rounding of basic arithmetic operations. Journal of Formalized Reasoning, 7(1):131–142, 2014.MathSciNetGoogle Scholar
  40. [534]
    D. M. Russinoff. A mechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. LMS Journal of Computation and Mathematics, 1:148–200, 1998.MathSciNetCrossRefGoogle Scholar
  41. [535]
    D. M. Russinoff. A mechanically checked proof of correctness of the AMD K5 floating point square root microcode. Formal Methods in System Design, 14(1):75–125, 1999.CrossRefGoogle Scholar
  42. [536]
    D. M. Russinoff. A case study in formal verification of register-transfer logic with ACL2: The floating point adder of the AMD Athlon processor. Lecture Notes in Computer Science, 1954:3–36, 2000.Google Scholar
  43. [540]
    J. Sawada and R. Gamboa. Mechanical verification of a square root algorithm using Taylor’s theorem. In 4th International Conference on Formal Methods in Computer-Aided Design (FMCAD), volume 2517 of Lecture Notes in Computer Science, pages 274–291, 2002.CrossRefGoogle Scholar
  44. [563]
    A. Solovyev, C. Jacobsen, Z. Rakamarić, and G. Gopalakrishnan. Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions. In 20th International Symposium on Formal Methods (FM), June 2015.CrossRefGoogle Scholar
  45. [647]
    R. Zumkeller. Formal global optimisation with Taylor models. In 3th International Joint Conference on Automated Reasoning (IJCAR), volume 4130 of Lecture Notes in Computer Science, pages 408–422, August 2006.CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Jean-Michel Muller
    • 1
  • Nicolas Brunie
    • 2
  • Florent de Dinechin
    • 3
  • Claude-Pierre Jeannerod
    • 4
  • Mioara Joldes
    • 5
  • Vincent Lefèvre
    • 4
  • Guillaume Melquiond
    • 6
  • Nathalie Revol
    • 4
  • Serge Torres
    • 7
  1. 1.CNRS - LIPLyonFrance
  2. 2.KalrayGrenobleFrance
  3. 3.INSA-Lyon - CITIVilleurbanneFrance
  4. 4.Inria - LIPLyonFrance
  5. 5.CNRS - LAASToulouseFrance
  6. 6.Inria - LRIOrsayFrance
  7. 7.ENS-Lyon - LIPLyonFrance

Personalised recommendations