Formal verification of exact computations using Newton's method

Nicolas Julien 1, * Ioana Pasca 1
* Auteur correspondant
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We are interested in the certification of Newton's method. We use a formalization of the convergence and stability of the method done with the axiomatic real numbers of Coq's Standard Library in order to validate the computation with Newton's method done with a library of exact real arithmetic based on co-inductive streams. The contribution of this work is twofold. Firstly, based on Newton's method, we design and prove correct an algorithm on streams for computing the root of a real function in a lazy manner. Secondly, we prove that rounding at each step in Newton's method still yields a convergent process with an accurate correlation between the precision of the input and that of the result. An algorithm including rounding turns out to be much more efficient.
Type de document :
Communication dans un congrès
Theorem Proving in Higher Order Logics, Aug 2009, Munich, Germany. Springer, 5674, pp.408-423, 2009, LNCS. 〈10.1007/978-3-642-03359-9_28〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00369511
Contributeur : Ioana Pasca <>
Soumis le : vendredi 20 mars 2009 - 10:39:05
Dernière modification le : jeudi 11 janvier 2018 - 16:19:55
Document(s) archivé(s) le : vendredi 12 octobre 2012 - 14:00:18

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Nicolas Julien, Ioana Pasca. Formal verification of exact computations using Newton's method. Theorem Proving in Higher Order Logics, Aug 2009, Munich, Germany. Springer, 5674, pp.408-423, 2009, LNCS. 〈10.1007/978-3-642-03359-9_28〉. 〈inria-00369511〉

Partager

Métriques

Consultations de la notice

350

Téléchargements de fichiers

490