Formal verification of exact computations using Newton's method - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2009

Formal verification of exact computations using Newton's method

Ioana Pasca
  • Fonction : Auteur
  • PersonId : 845903

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (203.48 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00369511 , version 1 (20-03-2009)

Identifiants

Citer

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

Collections

INRIA INRIA2
162 Consultations
432 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More