Programmes d’éléments finis formellement vérifié
Axe:SciLex 2&3
Coordinatrice :Sylvie Boldo, Inria
Objectif : Preuve de correction de la bibliothèque FELiScE implantant la méthode des éléments finis pour la résolution numérique d’équations aux dérivées partielles
Productions Scientifiques : publication et preuves Coq
Financement Labex en : 2014/2015 et 2015/2016
Documents : Lien vers le projet soumis à la commission Recherche
Présentation:
Le projet ELFIC se concentre sur la preuve de correction de la bibliothèque FELiScE (Finite Elements for Life Sciences and Engineering), implantant en C++ la méthode des éléments finis (MEF) pour la résolution numérique d’équations aux dérivées partielles (EDP), qui sont au coeur de nombreux programmes de simulation dans l’industrie. Sa vérification formelle augmentera la confiance dans tous les codes qui l’utilisent. Les méthodes de vérification développées dans ce projet représenteront une avancée à la fois pour la MEF elle-même, mais aussi pour la sûreté de logiciels critiques utilisant des algorithmes numériques complexes. Ce projet est interdisciplinaire (logique/preuve de programmes/analyse numérique) et ambitieux car le but est de vérifier formellement une bibliothèque réellement utilisée en analyse numérique en apportant la preuve formelle de convergence de ses algorithmes, la correction de son implantation C++ et l’analyse des erreurs d’arrondis.
Equipes concernées
- Inria Saclay – Île-de-France, équipe Toccata: Sylvie Boldo, Claude Marché, Guillaume Melquiond
- Ecole Polytechnique, LIX: Eric Goubault, Sylvie Putot
- CEA LIST: Franck Védrine, Virgile Prévosto
- Inria Paris – Rocquencourt, équipe Pomdapi: François Clément, Pierre Weis
- Université Paris 13, LIPN (Laboratoire d’informatique de Paris Nord): Micaela Mayero
- UTC, LMAC (Laboratoire de Mathématiques Appliquées de Compiègne): Vincent Martin
Réunions de travail:
- 12/11/14: kick-off
- 22/01/15: vérification formelle du programme de résolution de l’équation des ondes 1D (S. Boldo)
- 27/01/15: présentation de la bibliothèque Felisce implémentant la méthode des élémenst finis (V. Martin)
- 19/05/15 : Numerical theorem proving using polynomial interval arithmetic (Michal Konečný, Aston University, Birmingham, UK)- salle 435 (salle des thèses) au PCRI/Ada Lovelace 650