Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program
J. Autom. Reasoning, pp. 423-456, 2013.
Formal proof of numerical programConvergence of numerical schemeProof of C programCoq formal proofAcoustic wave equationMore(2+)
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 specif...More
PPT (Upload PPT)