Weitere Kapitel dieses Buchs durch Wischen aufrufen
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.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten
Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:
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
G. Barrett. Formal methods applied to a floating-point system. IEEE Transactions on Software Engineering, 15(5):611–621, 1989. CrossRef
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
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.
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
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.
S. Boldo and G. Melquiond. Computer Arithmetic and Formal Proofs. ISTE Press – Elsevier, 2017.
S. Boldo and C. Muñoz. Provably faithful evaluation of polynomials. In ACM Symposium on Applied Computing, pages 1328–1332, Dijon, France, 2006.
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.
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.
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.
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.
S. A. Figueroa. When is double rounding innocuous? ACM SIGNUM Newsletter, 30(3), 1995.
J. Harrison. Floating-point verification in HOL light: The exponential function. Technical Report 428, University of Cambridge Computer Laboratory, 1997.
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.
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.
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.
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.
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
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.
J. E. Holm. Floating-Point Arithmetic and Program Correctness Proofs. Ph.D. thesis, Cornell University, 1980.
C. Jacobi and C. Berg. Formal verification of the VAMP floating point unit. Formal Methods in System Design, 26(3):227–266, 2005. CrossRef
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
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
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.
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.
D. M. Priest. Algorithms for arbitrary precision floating point arithmetic. In 10th IEEE Symposium on Computer Arithmetic (ARITH-10), pages 132–143, June 1991.
P. Roux. Innocuous double rounding of basic arithmetic operations. Journal of Formalized Reasoning, 7(1):131–142, 2014. MathSciNet
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
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.
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
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
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
- Verifying Floating-Point Algorithms
Florent de Dinechin
- Chapter 13
Neuer Inhalt/© ITandMEDIA