14h00: Preuves formelles et équation des ondes. Sylvie Boldo, Projet Proval, Inria Saclay - Ile-de France.

Le but de ce travail est de prouver formellement et complètement (erreur de méthode et erreurs d'arrondi) de vrais programmes numériques. Nous commençons modestement avec la résolution de l'équation des ondes en utilisant un programme C de François Clément et la plateforme Why. Borner les erreurs dues aux calculs flottants nécessite une technique originaleur car les erreurs de calcul se compensent de façon très importante Borner l'erreur de méthode est un résultat classique de la littérature mais recèle de nombreux problèmes de définitions et d'imprécisions. Ce travail a été effectué avec François Clément, Jean-Christophe Filliâtre et Micaela Mayero dans le cadre de l'ANR blanche CerPAN.