Wave equation numerical resolution: a comprehensive mechanized proof of a C program - Archive ouverte HAL Access content directly
Journal Articles Journal of Automated Reasoning Year : 2013

Wave equation numerical resolution: a comprehensive mechanized proof of a C program

(1, 2) , (3) , (1, 2) , (4, 5) , (1, 2) , (3)
1
2
3
4
5

Abstract

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.
Fichier principal
Vignette du fichier
RR-7826.pdf (799.76 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00649240 , version 1 (07-12-2011)
hal-00649240 , version 2 (15-05-2012)
hal-00649240 , version 3 (12-07-2012)

Identifiers

Cite

Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, et al.. Wave equation numerical resolution: a comprehensive mechanized proof of a C program. Journal of Automated Reasoning, 2013, 50 (4), pp.423-456. ⟨10.1007/s10817-012-9255-4⟩. ⟨hal-00649240v3⟩
1208 View
636 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More