Issue No. 02 - February (2009 vol. 58)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2008.200
Sylvie Boldo , INRIA, ORSAY
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.
Floating point, discriminant, formal proof, Why platform, Coq.
Sylvie Boldo, "Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven", IEEE Transactions on Computers, vol. 58, no. , pp. 220-225, February 2009, doi:10.1109/TC.2008.200