Skip to main content
SpringerLink
Log in

Verifying Floating-Point Algorithms

  • Chapter
  • First Online:
Handbook of Floating-Point Arithmetic

  • 2667 Accesses

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.

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 129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover 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

Notes

  1. 1.

    Both floating-point signed zeros are mapped to the same real zero, so the conversion function is not injective.

  2. 2.

    When arithmetic operations produce a trap in case of exception, the proof is straightforward; but the way the traps are handled must also be verified (the absence of correct trap handling was one of the causes of the explosion of Ariane 5 in 1996). Another way is to prove that all the infinitely precise values are outside the domain of exceptional behaviors.

  3. 3.

    http://www.cs.utexas.edu/users/moore/acl2/.

  4. 4.

    One could certainly devise a rounding operator that has irrational breakpoints. Fortunately, none of the standard modes is that vicious.

  5. 5.

    https://www.cs.ox.ac.uk/tom.melham/res/forte.html.

  6. 6.

    http://pvs.csl.sri.com/.

  7. 7.

    https://hol-theorem-prover.org/.

  8. 8.

    http://www.cl.cam.ac.uk/~jrh13/hol-light/.

  9. 9.

    http://coq.inria.fr/.

  10. 10.

    http://flocq.gforge.inria.fr/.

  11. 11.

    http://coq-interval.gforge.inria.fr/.

  12. 12.

    https://github.com/soarlab/FPTaylor.

  13. 13.

    http://gappa.gforge.inria.fr/.

  14. 14.

    Verifying the numerical accuracy of an implementation is often only a small part of a verification effort. One may also have to prove that there are no infinite loops, no accesses out of the bounds of an array, and so on. So the user has to perform and combine various proofs in order to get a complete verification.

  15. 15.

    So Ω+ would be the successor of Ω if the exponent range was unbounded.

  16. 16.

    Making use of that equality requires to prove that u, v, and \(\tilde{v}\) are nonzero. Section 13.3.4 details how Gappa eliminates these hypotheses by using a slightly modified definition of the relative error.

  17. 17.

    Encountering the same formula is not unexpected: taking \(z =\tilde{ u} \times \tilde{ v}\), \(y =\tilde{ u} \times v\), and x = u Ă— v makes it appear.

  18. 18.

    With this C code, this is guaranteed by the ISO C standard under the condition that FLT_EVAL_METHOD is equal to 0 (see Section 6.2.3) and that floating-point expressions are not contracted (in particular because an FMA could be used here, see Section 6.2.3.2).

  19. 19.

    Gappa never assumes that a divisor cannot be zero, unless running in unconstrained mode.

References

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

    Article  Google Scholar 

  2. G. Barrett. Formal methods applied to a floating-point system. IEEE Transactions on Software Engineering, 15(5):611–621, 1989.

    Article  Google Scholar 

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

    Chapter  Google Scholar 

  4. S. Boldo. Kahan’s algorithm for a correct discriminant computation at last formally proven. IEEE Transactions on Computers, 58(2):220–225, 2009.

    Article  MathSciNet  Google Scholar 

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

    Chapter  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  9. 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. S. Boldo and G. Melquiond. Computer Arithmetic and Formal Proofs. ISTE Press – Elsevier, 2017.

    Google Scholar 

  11. S. Boldo and J.-M. Muller. Exact and approximated error of the FMA. IEEE Transactions on Computers, 60(2):157–164, 2011.

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  15. 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. M. Daumas and G. Melquiond. Certification of bounds on expressions involving rounded operators. Transactions on Mathematical Software, 37(1):1–20, 2010.

    Article  MathSciNet  Google Scholar 

  17. 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. 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. S. A. Figueroa. When is double rounding innocuous? ACM SIGNUM Newsletter, 30(3), 1995.

    Google Scholar 

  20. J. Harrison. Floating-point verification in HOL light: The exponential function. Technical Report 428, University of Cambridge Computer Laboratory, 1997.

    Google Scholar 

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

    Chapter  Google Scholar 

  26. 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. J. E. Holm. Floating-Point Arithmetic and Program Correctness Proofs. Ph.D. thesis, Cornell University, 1980.

    Google Scholar 

  28. C. Jacobi and C. Berg. Formal verification of the VAMP floating point unit. Formal Methods in System Design, 26(3):227–266, 2005.

    Article  Google Scholar 

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

    Article  Google Scholar 

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

    Article  Google Scholar 

  31. É. 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.

    Article  MathSciNet  Google Scholar 

  32. É. Martin-Dorel, G. Melquiond, and J.-M. Muller. Some issues related to double rounding. BIT Numerical Mathematics, 53(4):897–924, 2013.

    Article  MathSciNet  Google Scholar 

  33. 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. G. Melquiond. Floating-point arithmetic in the Coq system. Information and Computation, 216:14–23, 2012.

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  36. C. Muñoz and A. Narkawicz. Formalization of Bernstein polynomials and applications to global optimization. Journal of Automated Reasoning, 51(2):151–196, 2013.

    Article  MathSciNet  Google Scholar 

  37. 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. 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. P. Roux. Innocuous double rounding of basic arithmetic operations. Journal of Formalized Reasoning, 7(1):131–142, 2014.

    MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Article  Google Scholar 

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

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CNRS - LIP, Lyon, France

    Jean-Michel Muller

  2. Kalray, Grenoble, France

    Nicolas Brunie

  3. INSA-Lyon - CITI, Villeurbanne, France

    Florent de Dinechin

  4. Inria - LIP, Lyon, France

    Claude-Pierre Jeannerod, Vincent Lefèvre & Nathalie Revol

  5. CNRS - LAAS, Toulouse, France

    Mioara Joldes

  6. Inria - LRI, Orsay, France

    Guillaume Melquiond

  7. ENS-Lyon - LIP, Lyon, France

    Serge Torres

Authors
  1. Jean-Michel Muller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nicolas Brunie
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Florent de Dinechin
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Claude-Pierre Jeannerod
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Mioara Joldes
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Vincent Lefèvre
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Guillaume Melquiond
    View author publications

    You can also search for this author in PubMed Google Scholar

  8. Nathalie Revol
    View author publications

    You can also search for this author in PubMed Google Scholar

  9. Serge Torres
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Muller, JM. et al. (2018). Verifying Floating-Point Algorithms. In: Handbook of Floating-Point Arithmetic. Birkhäuser, Cham. https://doi.org/10.1007/978-3-319-76526-6_13

Download citation

Publish with us

Policies and ethics

Search

Navigation