Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Introduction Kapitel lesen Erstes Kapitel lesen

2018 | OriginalPaper | Buchkapitel

13. Verifying Floating-Point Algorithms

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

Erschienen in: Handbook of Floating-Point Arithmetic

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Interval Arithmetic
Nächstes Kapitel Extending the Precision
Fußnoten
1
Both floating-point signed zeros are mapped to the same real zero, so the conversion function is not injective.
 
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.
 
4
One could certainly devise a rounding operator that has irrational breakpoints. Fortunately, none of the standard modes is that vicious.
 
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
So Ω+ would be the successor of Ω if the exponent range was unbounded.
 
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
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
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
Gappa never assumes that a divisor cannot be zero, unless running in unconstrained mode.
 
Literatur
[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.CrossRef
[31]
G. Barrett. Formal methods applied to a floating-point system. IEEE Transactions on Software Engineering, 15(5):611–621, 1989.CrossRef
[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.CrossRef
[43]
S. Boldo. Kahan’s algorithm for a correct discriminant computation at last formally proven. IEEE Transactions on Computers, 58(2):220–225, 2009.MathSciNetCrossRef
[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.
[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.CrossRef
[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.MathSciNetCrossRef
[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.MathSciNetCrossRef
[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.
[54]
S. Boldo and G. Melquiond. Computer Arithmetic and Formal Proofs. ISTE Press – Elsevier, 2017.
[55]
S. Boldo and J.-M. Muller. Exact and approximated error of the FMA. IEEE Transactions on Computers, 60(2):157–164, 2011.MathSciNetCrossRef
[56]
S. Boldo and C. Muñoz. Provably faithful evaluation of polynomials. In ACM Symposium on Applied Computing, pages 1328–1332, Dijon, France, 2006.
[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.
[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.MathSciNetCrossRef
[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.
[134]
M. Daumas and G. Melquiond. Certification of bounds on expressions involving rounded operators. Transactions on Mathematical Software, 37(1):1–20, 2010.MathSciNetCrossRef
[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.
[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.
[200]
S. A. Figueroa. When is double rounding innocuous? ACM SIGNUM Newsletter, 30(3), 1995.
[238]
J. Harrison. Floating-point verification in HOL light: The exponential function. Technical Report 428, University of Cambridge Computer Laboratory, 1997.
[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.
[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.
[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.
[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.
[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.CrossRef
[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.
[261]
J. E. Holm. Floating-Point Arithmetic and Program Correctness Proofs. Ph.D. thesis, Cornell University, 1980.
[285]
C. Jacobi and C. Berg. Formal verification of the VAMP floating point unit. Formal Methods in System Design, 26(3):227–266, 2005.CrossRef
[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.CrossRef
[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.CrossRef
[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.MathSciNetCrossRef
[409]
É. Martin-Dorel, G. Melquiond, and J.-M. Muller. Some issues related to double rounding. BIT Numerical Mathematics, 53(4):897–924, 2013.MathSciNetCrossRef
[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.
[417]
G. Melquiond. Floating-point arithmetic in the Coq system. Information and Computation, 216:14–23, 2012.MathSciNetCrossRef
[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.MathSciNetCrossRef
[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.MathSciNetCrossRef
[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.
[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.
[516]
P. Roux. Innocuous double rounding of basic arithmetic operations. Journal of Formalized Reasoning, 7(1):131–142, 2014.MathSciNet
[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.MathSciNetCrossRef
[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.CrossRef
[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.
[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.CrossRef
[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.CrossRef
[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.CrossRef
Metadaten
Titel
Verifying Floating-Point Algorithms
verfasst von
Jean-Michel Muller
Nicolas Brunie
Florent de Dinechin
Claude-Pierre Jeannerod
Mioara Joldes
Vincent Lefèvre
Guillaume Melquiond
Nathalie Revol
Serge Torres
Copyright-Jahr
2018
Buch
Handbook of Floating-Point Arithmetic

Print ISBN: 978-3-319-76525-9

Electronic ISBN: 978-3-319-76526-6

Copyright-Jahr: 2018

DOI
https://doi.org/10.1007/978-3-319-76526-6_13