# ELEFFAN project

**Axis**: SciLex

**Subject**: Stability(s): links between floating arithmetic and numerical analysis

**Thesis Supervisors**: Sylvie Boldo (Inria - LRI) et Alexandre Chapoutot (ENSTA ParisTech)

**Institutions**: Inria - LRI et ENSTA ParisTech

**Administrator laboratory**: Inria

**PhD**: Florian Faissole

**Beginning**: 10/01/16

**Scientific production**:

**2019****Journal paper**- Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods. Sylvie Boldo, Florian Faissole, and Alexandre Chapoutot. Accepted for publication in IEEE Transactions on Computers, 8 pages, April 2019.

**Conference paper**- Formalisation en Coq des erreurs d'arrondi de méthodes de Runge-Kutta pour les systèmes matriciels. Florian Faissole. In 18èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, pages 19-26, Toulouse, France, June 2019.

**Poster communication**- Formalizing Loop-Carried Dependencies in Coq for High-Level Synthesis. Florian Faissole, George A. Constantinides, and David Thomas. Poster session of 27th IEEE Annual International Symposium on Field-Programmable Custom Computing Machines, San Diego, United States of America, April 2019.

**2018****Conference papers**- A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers, Sylvie Boldo, Florian Faissole, Vincent Tourneur, 25th IEEE Symposium on Computer Arithmetic, Jun 2018, Amherst, MA, United States
- Preuves constructives de programmes probabilistes, Florian Faissole, Bas Spitters, JFLA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France. 2018, 29èmes Journées Francophones des Langages Applicatifs. 〈https://www.lri.fr/~sboldo/JFLA18/〉
- Définir le fini : deux formalisations d'espaces de dimension finie, Florian Faissole, JLFA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-mer, France. pp.1-6, 2018, 29èmes Journées Francophones des Langages Applicatifs

**Preprints, Working Papers, ...**- Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods, Sylvie Boldo, Florian Faissole, Alexandre Chapoutot, 2018

**2017****Conference papers**- Formalization and closedness of finite dimensional subspaces, Florian Faissole, SYNASC 2017 - 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2017, Timișoara, Romania. pp.1-7
- Round-off Error Analysis of Explicit One-Step Numerical Integration Methods, Sylvie Boldo, Florian Faissole, Alexandre Chapoutot, 24th IEEE Symposium on Computer Arithmetic, Jul 2017, London, United Kingdom.〈http://arith24.arithsymposium.org/〉.〈10.1109/ARITH.2017.22〉
- Preuve formelle du théorème de Lax–Milgram, Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero, 16èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2017, Montpellier, France. 〈http://afadl2017.imag.fr/〉
- Synthetic topology in HoTT for probabilistic programming, Florian Faissole, Bas Spitters, The Third International Workshop on Coq for Programming Languages (CoqPL 2017), Jan 2017, Paris, France. 〈http://conf.researchr.org/track/POPL-2017/CoqPL-2017-papers〉
- A Coq formal proof of the Lax–Milgram theorem, Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero, 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Jan 2017, Paris, France. 〈http://cpp2017.mpi-sws.org/〉. 〈10.1145/3018610.3018625〉

**Poster communications**- Synthetic topology in homotopy type theory for probabilistic programming, Florian Faissole, Bas Spitters, PPS 2017 - Workshop on probabilistic programming semantics , Jan 2017, Paris, France. pp.3 BibTex

**Ressources**:

**Autre page du projet ELEFFAN**—

**Page web de Florian Faissole**

**Context**:

This topic is at the interface between computer science and applied mathematics. The computer part is preponderant because it is a question here of considering algorithms resulting from numerical analysis and to check their good behavior on computer. This behaviour, proven on the assumption that the calculations are perfect, could be put in default by rounding and capacity overruns due to calculations in floating arithmetic.

**Scientific goals**:

Computer calculations create errors with each calculation that can accumulate to give a completely false result in certain pathological cases. This thesis aims to clarify the link between two notions: stability in the sense of numerical analysis and stability in the sense of floating arithmetic. In floating arithmetic, an algorithm is stable if, on close inputs, it provides close outputs. The ratio between the difference in inputs and the difference in outputs is called conditioning, and it characterizes the stability of a function. In numerical analysis, stability has another meaning. For partial differential equations, this means that the solution values do not diverge. For ordinary differential equations, this means the stability of the dynamic system, and often Lyapunov's stability. Note that there is also a notion of data sensitivity for numerical integration schemes called zero-stability that is very similar to the notion of stability in floating numbers. This thesis may highlight this link before considering the other types of stability of digital schemas.

**Perspectives**:

Mathematicians believe that a stable pattern in the sense of dynamics is numerically stable. We think this recipe is true, and we would like to prove it formally. The idea is that the numerical errors will be compensated because of the particular form that a stable and convergent numerical schema has and thus that the calculation will globally "go well". Local rounding errors can easily be bounded at each step by the floating arithmetic properties specified by IEEE-754 (with the exception of trigonometric functions). This is particularly simple here because the values are bounded by the stability of the schematic. One difficulty will be to limit the final errors after a large number of iterations. In fact, it appears that the offsets exhibited in a particular case are more general and in fact apply to a broad class of stable digital schemes. Another difficulty is that the result must be general enough to apply to different types of schemas, but precise enough to give usable error bounds on rounding errors.