Le projet MILC

Le projet MILC est un projet DIM-RFSI 2018.

La résolution des équations aux dérivées partielles (EDP) est au cœur de nombreux programmes de simulation dans l'industrie et la méthode des éléments finis (MEF) est un outil très populaire pour leur résolution numérique.

Le but à long terme dans lequel s'inscrit ce projet se situe dans le domaine de la sécurité, de la fiabilité et de la sûreté. Il s'agit de poser les fondements qui nous permettront de prouver la correction d'une bibliothèque implantant la MEF en C++, telle que FELiScE (Finite Elements for Life Sciences and Engineering). Sa vérification formelle augmentera la confiance dans tous les codes qui l'utilisent. Ce projet est interdisciplinaire (logique/preuve de programmes/analyse numérique).

Ces preuves reposent entre autres sur la théorie de la mesure, l'intégrale de Lebesgue, les distributions et les espaces de Sobolev. Durant la période de ce projet, nous nous proposons de formaliser et prouver en Coq les bases mathématiques jusqu'à la construction de l'espace fonctionnel L² ainsi que les propriétés afférentes, en particulier la complétude pour la norme associée au produit scalaire.