Kahan's algorithm for a correct discriminant computation at last formally proven

Sylvie Boldo 1, 2
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : This article tackles Kahan's algorithm to compute accurately the discriminant whatever the inputs. This is a known difficult problem and this algorithm leads to an error bounded by 2 ulps of the result. The proofs involved are long and tricky and even trickier than expected as the test involved may give an unexpected result. We give here the total demonstration of the validity of this algorithm and we provide sufficient conditions to guarantee neither Overflow, nor Underflow will jeopardize the result. The program was annotated using the Caduceus tool and the proof obligations were done using the Coq automatic proof checker.
Type de document :
Article dans une revue
IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2009, 58 (2), pp.220-225. <10.1109/TC.2008.200>
Liste complète des métadonnées


https://hal.inria.fr/inria-00171497
Contributeur : Sylvie Boldo <>
Soumis le : mardi 24 novembre 2009 - 11:00:56
Dernière modification le : jeudi 9 février 2017 - 15:53:01
Document(s) archivé(s) le : samedi 26 novembre 2016 - 16:30:53

Fichier

boldo.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

Sylvie Boldo. Kahan's algorithm for a correct discriminant computation at last formally proven. IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2009, 58 (2), pp.220-225. <10.1109/TC.2008.200>. <inria-00171497v2>

Partager

Métriques

Consultations de
la notice

406

Téléchargements du document

248