Formal verification of exact computations using Newton's method - Archive ouverte HAL Access content directly
Conference Papers Year : 2009

Formal verification of exact computations using Newton's method

(1) , (1)
Ioana Pasca
  • Function : Author
  • PersonId : 845903


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
Origin : Files produced by the author(s)

Dates and versions

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



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⟩


142 View
412 Download



Gmail Facebook Twitter LinkedIn More