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

TL;DR

This paper presents a fully mechanized proof of correctness for a C program solving the 1D acoustic wave equation, combining formal verification of numerical and floating-point errors using multiple proof tools.

Contribution

It introduces the first fully machine-checked numerical analysis of a wave equation solver, integrating formal proofs of correctness, method errors, and round-off errors.

Findings

The C implementation is proven correct and sound with respect to the numerical scheme.

Errors are rigorously bounded using formal methods and SMT solvers.

This work demonstrates the feasibility of fully verified numerical software for PDEs.

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.