Wave Equation Numerical Resolution: Mathematics and Program

Sylvie Boldo 1, 2 Francois Clement 3 Jean-Christophe Filliâtre 1, 2 Micaela Mayero 4, 5 Guillaume Melquiond 1, 2 Pierre Weis 3
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
4 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : We formally prove the C program that implements a simple 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 the floating-point computation leads to round-off errors. We formally specify in Coq the numerical scheme, prove both the method error and the round-off error of the program, and derive an upper bound for the total error. This proves the adequacy of the C program to the numerical scheme and the convergence of the effective computation. To our knowledge, this is the first time a numerical analysis program is fully machine-checked.
Complete list of metadatas

https://hal.inria.fr/hal-00649240
Contributor : Francois Clement <>
Submitted on : Wednesday, December 7, 2011 - 4:26:23 PM
Last modification on : Tuesday, February 5, 2019 - 3:12:18 PM
Long-term archiving on : Friday, November 16, 2012 - 2:45:09 PM

Files

RR-7826.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00649240, version 1
  • ARXIV : 1112.1795

Collections

Citation

Sylvie Boldo, Francois Clement, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, et al.. Wave Equation Numerical Resolution: Mathematics and Program. [Research Report] RR-7826, 2011, pp.30. ⟨hal-00649240v1⟩

Share

Metrics

Record views

164

Files downloads

91