Skip to Main content Skip to Navigation
New interface
Journal articles

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.
Complete list of metadata

Cited literature [52 references]  Display  Hide  Download
Contributor : Francois Clement Connect in order to contact the contributor
Submitted on : Thursday, July 12, 2012 - 10:41:13 AM
Last modification on : Tuesday, October 25, 2022 - 4:19:17 PM
Long-term archiving on: : Thursday, December 15, 2016 - 10:36:35 PM


Files produced by the author(s)



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⟩



Record views


Files downloads