Preuves formelles de la résolution numérique de l'équation des ondes 1D

Cet exposé montrera les résultats du projet FOST: nous avons formellement prouvé un programme C implémentant un schéma numérique simple pour la résolution de l'équation des ondes acoustiques en dimension 1. Nous avons annoté ce programme et l'avons complètement prouvé. Cela inclut l'absence d'erreur à l'exécution, la majoration mathématique usuelle de l'erreur de méthode due au schéma numérique et une borne sur les erreurs d'arrondi.