Name
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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/s10817-012-9255-4 | J. Autom. Reasoning |
Keywords | Field | DocType |
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 | Discrete mathematics,Acoustic wave equation,Algorithm,Numerical resolution,Soundness,Wave equation,Numerical analysis,Partial differential equation,Mathematics,Computation | Journal |
Volume | Issue | ISSN |
50 | 4 | Journal of Automated Reasoning 50, 4 (2013) 423-456 |
Citations | PageRank | References |
24 | 1.00 | 27 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sylvie Boldo | 1 | 292 | 26.85 |
| François Clément | 2 | 37 | 4.04 |
| Jean-Christophe Filliâtre | 3 | 615 | 45.86 |
| Micaela Mayero | 4 | 84 | 10.38 |
| Guillaume Melquiond | 5 | 345 | 24.82 |
| Pierre Weis | 6 | 151 | 19.20 |