Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download
Contributor : Ioana Pasca <>
Submitted on : Friday, March 20, 2009 - 10:39:05 AM
Last modification on : Thursday, March 5, 2020 - 5:34:18 PM
Document(s) archivé(s) le : Friday, October 12, 2012 - 2:00:18 PM


Files produced by the author(s)




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⟩



Record views


Files downloads