The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.02 - February (2009 vol.58)
pp: 220-225
Sylvie Boldo , INRIA, ORSAY
ABSTRACT
This article tackles Kahan's algorithm to compute accurately the discriminant. This is a known difficult problem, and this algorithm leads to an error bounded by 2 ulps of the floating-point result. The proofs involved are long and tricky and even trickier than expected as the test involved may give a result different from the result of the same test without rounding. We give here the total demonstration of the validity of this algorithm, and we provide sufficient conditions to guarantee that neither overflow nor underflow will jeopardize the result. The IEEE-754 double-precision program is annotated using the Why platform and the proof obligations are done using the Coq automatic proof checker.
INDEX TERMS
Floating point, discriminant, formal proof, Why platform, Coq.
CITATION
Sylvie Boldo, "Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven", IEEE Transactions on Computers, vol.58, no. 2, pp. 220-225, February 2009, doi:10.1109/TC.2008.200
REFERENCES
[1] T.J. Dekker, “A Floating Point Technique for Extending the Available Precision,” Numerische Mathematik, vol. 18, no. 3, pp. 224-242, 1971.
[2] S. Boldo and M. Daumas, “A Mechanically Validated Technique for Extending the Available Precision,” Proc. 35th Asilomar Conf. Signals, Systems, and Computers, pp. 1299-1303, http://perso.ens-lyon.fr/marc. daumas/SoftArith BolDau01b.pdf, 2001.
[3] F. de Dinechin, C.Q. Lauter, and J.-M. Muller, “Fast and Correctly Rounded Logarithms in Double-Precision,” Theoretical Informatics and Applications, vol. 41, pp. 85-102, http://perso.ens-lyon.fr/florent.de. dinechin/ recherche/publis2007-TIA.pdf, 2007.
[4] L. Fousse, G. Hanrot, V. Lefèvre, P. Pélissier, and P. Zimmermann, “MPFR: A Multiple-Precision Binary Floating-Point Library with Correct Rounding,” ACM Trans. Math. Software, vol. 33, no. 2, p. 13, http://doi.acm.org/10.11451236463.1236468 , June 2007.
[5] S. Boldo and M. Daumas, “A Simple Test Qualifying the Accuracy of Horner's Rule for Polynomials,” Numerical Algorithms, vol. 37, nos. 1-4, pp.45-60, http://www.ingentaconnect.com/content/klu/ numa/2004/00000037/F004000105276602, 2004.
[6] N.J. Higham, Accuracy and Stability of Numerical Algorithms, SIAM, seconded., http://www.ma.man.ac.uk/~highamasna/, 2002.
[7] W. Kahan, On the Cost of Floating-Point Computation without Extra-Precise Arithmetic, p. 21, http://www.cs.berkeley.edu/~wkahanQdrtcs.pdf , Nov. 2004.
[8] L. Kettner, K. Mehlhorn, S. Pion, S. Schirra, and C.K. Yap, “Classroom Examples of Robustness Problems in Geometric Computations,” Proc. 12th European Symp. Algorithms (ESA '04), pp. 702-713, http://cgal.inria.fr/Publications/2004KMPSY04 , 2004.
[9] M. Daumas, L. Rideau, and L. Théry, “A Generic Library of Floating-Point Numbers and Its Application to Exact Computing,” Proc. 14th Int'l Conf. Theorem Proving in Higher Order Logics (TPHOLs '01), pp. 169-184, http://perso.ens-lyon.fr/marc.daumas/SoftArith DauRidThe01.ps, 2001.
[10] S. Boldo, “Preuves Formelles en Arithmétiques à Virgule Flottante,” PhD dissertation, École Normale Supérieure de Lyon, http://www.ens-lyon.fr/LIP/Pub/Rapports/ PhD/PhD2004PhD2004-05.pdf, Nov. 2004.
[11] J.-C. Filliâtre and C. Marché, “Multi-Prover Verification of C Programs,” Proc. Sixth Int'l Conf. Formal Eng. Methods (ICFEM '04), pp. 15-29, http://www.lri.fr/~filliatr/ftp/publiscaduceus.ps.gz , Nov. 2004.
[12] J.-C. Filliâtre and C. Marché, “The Why/Krakatoa/Caduceus Platform for Deductive Program Verification,” Proc. 19th Int'l Conf. Computer Aided Verification (CAV '07), W. Damm and H. Hermanns, eds., http://www.lri.fr/~filliatr/ftp/publiscav07.pdf , July 2007.
[13] S. Boldo and J.-C. Filliâtre, “Formal Verification of Floating-Point Programs,” Proc. 18th IEEE Symp. Computer Arithmetic (ARITH '07), P.Kornerup and J.-M. Muller, eds., pp. 187-194, June 2007.
[14] J.-M. Muller, On the Definition of ulp(x), Technical Report LIP RR2005-09 INRIA RR-5504, Laboratoire de l'Informatique du Parallélisme, ftp://ftp.inria.fr/INRIA/publication/publi-pdf/ RRRR-5504.pdf, 2005.
[15] G.W. Veltkamp, Algolprocedures voor het Berekenen van een Inwendig Product in Dubbele Precisie, RC-Informatie 22, Technische Hogeschool Eindhoven, 1968.
[16] G.W. Veltkamp, ALGOL Procedures voor het Rekenen in Dubbele Lengte, RC-Informatie 21, Technische Hogeschool Eindhoven, 1969.
[17] A.H. Karp and P. Markstein, “High-Precision Division and Square Root,” ACM Trans. Math. Software, vol. 23, no. 4, pp. 561-589, Dec. 1997.
[18] S. Boldo, “Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms,” Proc. Third Int'l Joint Conf. Automated Reasoning (IJCAR '06), pp. 52-66, Aug. 2006.
[19] S. Boldo, M. Daumas, W. Kahan, and G. Melquiond, “Proof and Certification for an Accurate Discriminant,” Proc. 12th IMACS-GAMM Int'l Symp. Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN '06), Sept. 2006.
[20] P.H. Sterbenz, Floating Point Computation. Prentice Hall, 1974.
[21] G. Melquiond and S. Pion, “Formally Certified Floating-Point Filters for Homogeneous Geometric Predicates,” Theoretical Informatics and Applications, vol. 41, no. 1, pp. 57-70, http://perso.ens-lyon.fr/guillaume. melquiond/ doc07-tia.pdf, 2007.
35 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool