Formal verification of exact computations using Newton's method

Nicolas Julien 1, * Ioana Pasca 1
* Corresponding author
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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/inria-00369511
Contributor : Ioana Pasca <>
Submitted on : Friday, March 20, 2009 - 10:39:05 AM
Last modification on : Thursday, January 11, 2018 - 4:19:55 PM
Long-term archiving on : Friday, October 12, 2012 - 2:00:18 PM

File

main.pdf
Files produced by the author(s)

Identifiers

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. pp.408-423, ⟨10.1007/978-3-642-03359-9_28⟩. ⟨inria-00369511⟩

Share

Metrics

Record views

395

Files downloads

544