|
|
| Micaela Mayero
| |
|
Contacts: English version Last modified: Thu Mar 21 17:15:49 CEST 2024 |
Année 2018–2019 Proposition de stage
Titre : Mesure et Intégrale de Lebesgue en Coq
Lieu :
Personne encadrant le stage localement :
Co-encadrants :
Contexte : L’un des axes de l’équipe LoVe depuis plus de 10 ans est la formalisation et automatisation de preuves, notamment autour de l’analyse numérique et du développement de bibliothèques pour la vérification de programmes. L’une des approches pour certifier un programme est la vérification déductive, c’est-à-dire la preuve de propriétés logiques extraites du programme. Cela s’appuie sur une base de théorèmes formellement prouvés avec le système Coq. Ce stage fait partie du projet DIM-RFSI MILC1; le stagiaire pourra être amené à se rendre à l’INRIA Paris ou Saclay.
Objet du stage : La méthode des éléments finis pour la résolution numérique d’équations aux dérivées partielles est au cœur 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 méthode des éléments finis elle-même, mais aussi pour la sûreté de logiciels critiques utilisant des algorithmes numériques complexes. 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 FELiScE2 (Finite Elements for Life Sciences and Engineering). Ces preuves reposent entre autres sur la théorie de la mesure, l’intégrale de Lebesgue, les distributions et les espaces de Sobolev. Ce stage a pour but de prouver formellement en Coq un certain nombre de résultats mathématiques bien connus tels que la construction de l’espace fonctionnel L2 ainsi que les propriétés afférentes, en particulier la complétude pour la norme associée au produit scalaire. Ce n’est évidemment pas seulement une « traduction » de livres de mathématiques vers un assistant de preuves. Cela nécessitera de bien comprendre les preuves existantes de façon à les factoriser, les simplifier voire à les généraliser. Il faudra également choisir les bonnes formalisations pour simplifier les preuves ultérieures. Il faut noter que le stagiaire pourra se baser sur des travaux antérieurs concernant l’analyse réelle [BLM15] et la preuve formelle du théorème de Lax-Milgram [CPP2017] par exemple. Références
Ce document a été traduit de LATEX par HEVEA |