Dissertation/ Thesis
Formalizations of error analysis in numerical analysis and floating-point arithmetic ; Formalisations d’analyses d’erreurs en analyse numérique et en arithmétique à virgule flottante
| العنوان: | Formalizations of error analysis in numerical analysis and floating-point arithmetic ; Formalisations d’analyses d’erreurs en analyse numérique et en arithmétique à virgule flottante |
|---|---|
| المؤلفون: | Faissole, Florian |
| المساهمون: | Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Université Paris Saclay (COmUE), Sylvie Boldo |
| المصدر: | https://theses.hal.science/tel-02470728 ; Logique en informatique [cs.LO]. Université Paris Saclay (COmUE), 2019. Français. ⟨NNT : 2019SACLS594⟩. |
| بيانات النشر: | CCSD |
| سنة النشر: | 2019 |
| مصطلحات موضوعية: | Floating-point arithmetic, Rounding errors, Formal proofs, Coq, Runge-Kutta, Arithmétique à virgule flottante, Erreurs d'arrondi, Preuves formelles, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] |
| الوصف: | This thesis consists of three contributions related to the Coq formalization of error analysis in numerical analysis and floating-point arithmetic.First, we have exhibited an algorithm computing the average of two decimal floating-point numbers and have proved that this algorithm computes the correct rounding. We have formalized the algorithm and its correctness proof in the Coq proof assistant.The second contribution of the thesis is the analysis and the formalization of rounding error bounds associated to the implementation of Runge-Kutta methods applied to linear systems. We have proposed a generic methodology to build a bound on the error accumulated over the iterations, taking potential underflow and overflow into account. We have then instantiated this methodology forclassic Runge-Kutta methods, e.g. the Euler and RK2 methods. We have proposed a formalization of the results, including the definition of matrix norms, theproof of rounding error bounds for matrix operations and the formalization of the generic results and their instantiations.Finally, we have proposed a formalization of functional analysis results that serve as foundations for the finite element method. This formalization is based on the Coquelicot library and includes the theory of Hilbert spaces, the formal proof of the Lax--Milgram Theorem and the proof of completeness of finite dimensional subspaces of Hilbert spaces. ; Cette thèse est constituée de trois contributions liées à la formalisation en Coq d'analyses d'erreurs dans les domaines de l'analyse numérique et de l'arithmétique à virgule flottante.Nous avons tout d'abord proposé un algorithme calculant la moyenne de deux nombres flottants décimaux et avons montré que cet algorithme fournissait l'arrondi correct. Nous avons formalisé l'algorithme et sa preuve de correction dans l'assistant de preuves Coq.La seconde contribution de la thèse est l'analyse et la formalisation de bornes sur les erreurs d'arrondi d'implémentations de méthodes de Runge-Kutta appliquées à des systèmes ... |
| نوع الوثيقة: | doctoral or postdoctoral thesis |
| اللغة: | French |
| Relation: | NNT: 2019SACLS594 |
| الاتاحة: | https://theses.hal.science/tel-02470728 https://theses.hal.science/tel-02470728v1/document https://theses.hal.science/tel-02470728v1/file/84852_FAISSOLE_2019_archivage.pdf |
| Rights: | info:eu-repo/semantics/OpenAccess |
| رقم الانضمام: | edsbas.702A8049 |
| قاعدة البيانات: | BASE |
| الوصف غير متاح. |