Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program

Sylvie Boldo 1, 2 François Clément 3 Jean-Christophe Filliâtre 1, 2 Micaela Mayero 4, 5 Guillaume Melquiond 1, 2 Pierre Weis 3
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
5 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
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.
Document type :
Journal articles
Journal of Automated Reasoning, Springer Verlag, 2013, 50 (4), pp.423-456. <10.1007/s10817-012-9255-4>
Liste complète des métadonnées

https://hal.inria.fr/hal-00649240
Contributor : Francois Clement <>
Submitted on : Thursday, July 12, 2012 - 10:41:13 AM
Last modification on : Thursday, February 9, 2017 - 3:56:57 PM
Document(s) archivé(s) le : Thursday, December 15, 2016 - 10:36:35 PM

Files

RR-7826.pdf
Files produced by the author(s)

Identifiers

Citation

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, Springer Verlag, 2013, 50 (4), pp.423-456. <10.1007/s10817-012-9255-4>. <hal-00649240v3>

Share

Metrics

Record views

1101

Document downloads

403