Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program
Résumé
We formally prove correct a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and floating-point computations lead to round-off errors. We annotate this C program to specify both method error and round-off error. We use Frama-C to generate theorems that guarantee the soundness of the code. We discharge these theorems using SMT solvers, Gappa, and Coq. This involves a large Coq development to prove the adequacy of the C program to the numerical scheme and to bound errors. To our knowledge, this is the first time such a numerical analysis program is fully machine-checked.
Nous prouvons formellement la correction d'un programme C implémentant un schéma numérique pour la résolution de l'équation des ondes acoustiques en dimension 1. Une telle implémentation introduit différents types d'erreurs : l'erreur de méthode due au schéma numérique et l'erreur d'arrondi due aux calculs en virgule flottante. Nous annotons ce programme C pour spécifier ces deux types d'erreur. Nous utilisons Frama-C pour générer les théorèmes qui garantissent la correction du code. Nous prouvons ces théorèmes à l'aide de solveurs SMT, de Gappa et de Coq. Un développement Coq important est nécessaire pour prouver l'adéquation du programme C au schéma numérique et pour borner les erreurs. À notre connaissance, c'est la première fois qu'un tel programme d'analyse numérique est complètement vérifié mécaniquement.
Origine : Fichiers produits par l'(les) auteur(s)