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.
Document type :
Conference papers
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
Long-term archiving on: : 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