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.