Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program
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.
Cite
@article{arxiv.1112.1795,
title = {Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program},
author = {Sylvie Boldo and Francois Clement and Jean-Christophe Filliâtre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
journal= {arXiv preprint arXiv:1112.1795},
year = {2013}
}
Comments
No. RR-7826 (2011)