inria-00171497, version 2
Kahan's algorithm for a correct discriminant computation at last formally proven
Sylvie Boldo
a, 1, 2
IEEE Transactions on Computers 58, 2 (2009) 220-225
Résumé : 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.
- a – INRIA
- 1 : PROVAL (INRIA Saclay - Ile de France)
- INRIA – Université Paris XI - Paris Sud – CNRS : UMR
- 2 : Laboratoire de Recherche en Informatique (LRI)
- CNRS : UMR8623 – Université Paris XI - Paris Sud
- Domaine : Informatique/Logique en informatique
Informatique/Arithmétique des ordinateurs - Mots-clés : Floating-point – discriminant – formal proof.
- Versions disponibles : v1 (12-09-2007) v2 (24-11-2009)
- inria-00171497, version 2
- http://hal.inria.fr/inria-00171497
- oai:hal.inria.fr:inria-00171497
- Contributeur : Sylvie Boldo
- Soumis le : Mardi 24 Novembre 2009, 11:00:56
- Dernière modification le : Mardi 24 Novembre 2009, 16:27:26
Documents associés
Exporter