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.

No. RR-7826 (2011)

References in corpus (6)

• Certified Exact Transcendental Real Number Computation in Coq
• Hilbert's "Verunglueckter Beweis," the first epsilon theorem, and consistency proofs
• Type classes for efficient exact real arithmetic in Coq
• Formal Proof of a Wave Equation Resolution Scheme: the Method Error
• A computer verified, monadic, functional implementation of the integral
• Proof-irrelevant model of CC with predicative induction and judgmental equality

Cited by in corpus (6)

• Rounding Error Analysis of Linear Recurrences Using Generating Series
• Automatic generation and verification of test-stable floating-point code
• Computer-Assisted Verification of Four Interval Arithmetic Operators
• A formal proof of the Lax equivalence theorem for finite difference schemes
• An Abstraction-guided Approach to Scalable and Rigorous Floating-Point Error Analysis
• Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program