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

J. Autom. Reasoning, pp. 423-456, 2013.

Cited by: 47|Bibtex|Views13|Links
EI
Keywords:
Formal proof of numerical programConvergence of numerical schemeProof of C programCoq formal proofAcoustic wave equationMore(2+)

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 specif...More

Code:

Data:

Your rating :
0

 

Tags
Comments