 |
 |
|
|
| HAL : hal-00649240, version 3 |
| arXiv : 1112.1795 |
| DOI : 10.1007/s10817-012-9255-4 |
| Voir la fiche détaillée |  BibTeX,EndNote,... |
 |
| Journal of Automated Reasoning 50, 4 (2013) 423-456 |
|
|
| Versions disponibles | v1 (08-12-2011) | v2 (16-05-2012) | v3 (12-07-2012) |
|
|
|
|
| Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program |
|
|
| Sylvie Boldo 1, 2Francois Clement 3 |
|
|
| (04/2013) |
|
|
|
| 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. |
|
|
|
|
|
|
|
|
|
|
|
| 1 : | PROVAL (INRIA Saclay - Ile de France) |
|
|
|
INRIA – Université Paris XI - Paris Sud – CNRS : UMR |
|
|
| 2 : | Laboratoire de Recherche en Informatique (LRI) |
|
|
|
CNRS : UMR8623 – Université Paris XI - Paris Sud |
|
|
| 3 : | ESTIME (INRIA Paris-Rocquencourt) |
|
|
|
INRIA |
|
|
| 4 : | Laboratoire d'informatique de Paris-nord (LIPN) |
|
|
|
CNRS : UMR7030 – Université Paris XIII - Paris Nord |
|
|
| 5 : | ARENAIRE (Inria Grenoble Rhône-Alpes / LIP Laboratoire de l'Informatique du Parallélisme) |
|
|
|
INRIA – CNRS : UMR5668 – Université Claude Bernard - Lyon I – École Normale Supérieure - Lyon |
|
|
|
|
|
|
|
|
|
| Domaine | : | Informatique/Logique en informatique Mathématiques/Analyse numérique Informatique/Arithmétique des ordinateurs |
|
|
| Formal proof of numerical program – Convergence of numerical scheme – Proof of C program – Coq formal proof – Acoustic wave equation – Partial differential equation – Rounding error analysis |
|
|
|
| Liste des fichiers attachés à ce document : | ||||||||||
|
||||||||||
|
|
|
| hal-00649240, version 3 | |
| http://hal.inria.fr/hal-00649240 | |
| oai:hal.inria.fr:hal-00649240 | |
| Contributeur : Francois Clement | |
| Soumis le : Jeudi 12 Juillet 2012, 10:41:13 | |
| Dernière modification le : Mardi 26 Mars 2013, 11:15:56 | |
