Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Thèses et habilitations
Production scientifique
Doctorat de

Doctorat
Equipe : Vérification d'Algorithmes, Langages et Systèmes

Formalisations d'analyses d'erreurs en analyse numérique et en arithmétique à virgule flottante

Début le 01/10/2016
Direction : BOLDO, Sylvie

Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Sud

Lieu de déroulement : LRI -l'amphithéâtre du bâtiment 660 (Claude Shanno

Soutenue le 13/12/2019 devant le jury composé de :
Rapporteurs :

- Yves Bertot (Inria Sophia Antipolis Méditerranée),
- Paul Zimmermann (Inria Nancy Grand Est),

Examinateurs :

- Stef Graillat (Sorbonne Université),
- Florent Hivert (Université Paris-Sud),
- Assia Mahboubi (Inria, LS2N),

Encadrants :

- Sylvie Boldo (Inria Saclay - Île-de-France),
- Alexandre Chapoutot (ENSTA ParisTech),

Invité :

- David Mentré (Mitsubishi Electric R&D Centre Europe).

Activités de recherche :

Résumé :
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 linéaires. Nous avons proposé
une méthodologie générique permettant de construire une borne sur l'erreur d'arrondi accumulée au cours
des itérations et qui tient compte d'éventuels dépassements de capacité. Nous avons ensuite appliqué la
méthodologie à des méthodes de Runge-Kutta classiques, comme les méthodes d'Euler et de RK2. Nous
avons proposé une formalisation de l'analyse, incluant la définition de normes matricielles, la démonstration de bornes sur les erreurs d'arrondi d'opérations matricielles et la formalisation des résultats génériques et de leur instanciation.

Enfin, nous avons proposé la formalisation de résultats d'analyse fonctionnelle qui servent de fondements
à la méthode des éléments finis. Cette formalisation repose sur la bibliothèque Coquelicot et inclut la théorie des espaces de Hilbert, la formalisation du théorème de Lax-Milgram et la preuve de complétude des
sous-espaces de dimension finie d'espaces de Hilbert.