Wave Equation Numerical Resolution: Mathematics and Program

Sylvie Boldo; Francois Clement; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis

hal-00649240, version 1

Wave Equation Numerical Resolution: Mathematics and Program

Sylvie Boldo ()^c^, 1, 2, Francois Clement (, ) ³, Jean-Christophe Filliâtre ()^a^, 1, 2, Micaela Mayero ()^b^, 4, 5, Guillaume Melquiond ()^c^, 1, 2, Pierre Weis ()^c^, 3

N° RR-7826 (2011)

Résumé : 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.

a – CNRS
b – Université Paris-Nord - Paris XIII
c – INRIA
1 : PROVAL (INRIA Saclay - Ile de France)
INRIA – Université Paris XI - Paris Sud – CNRS : UMR
2 : Laboratoire de Recherche en Informatique (LRI)
CNRS : UMR8623 – Université Paris XI - Paris Sud
3 : ESTIME (INRIA Paris-Rocquencourt)
INRIA
4 : Laboratoire d'informatique de Paris-nord (LIPN)
CNRS : UMR7030 – Université Paris XIII - Paris Nord
5 : ARENAIRE (Inria Grenoble Rhône-Alpes / LIP Laboratoire de l'Informatique du Parallélisme)
INRIA – CNRS : UMR5668 – Université Claude Bernard - Lyon I – École Normale Supérieure - Lyon

hal-00649240, version 1
http://hal.inria.fr/hal-00649240
oai:hal.inria.fr:hal-00649240
Contributeur : Francois Clement <>
Soumis le : Mercredi 7 Décembre 2011, 16:26:23
Dernière modification le : Jeudi 8 Décembre 2011, 23:03:49

Voir la fiche détaillée

Documents associés

PDF :

PS :

arXiv : 1112.1795

Exporter

Bibtex EndNote TEI RefWorks

%F hal-00649240, version 1
%0 Report
%U http://hal.inria.fr/hal-00649240
%2 INFO:INFO_LO;MATH:MATH_NA
%T Wave Equation Numerical Resolution: Mathematics and Program
%A Boldo, Sylvie
%A Clement, Francois
%A Filliâtre, Jean-Christophe
%A Mayero, Micaela
%A Melquiond, Guillaume
%A Weis, Pierre
%+ PROVAL - INRIA Saclay - Ile de France , Laboratoire de Recherche en Informatique - LRI , ESTIME - INRIA Paris-Rocquencourt , Laboratoire d'informatique de Paris-nord - LIPN , ARENAIRE - Inria Grenoble Rhône-Alpes / LIP Laboratoire de l'Informatique du Parallélisme
%X 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.
%2 Nous prouvons formellement le programme C implémentant un schéma numérique simple pour la résolution de l'équation des ondes acoustiques en dimension 1. Une telle implémentation introduit différents types d'erreurs : l'erreur de méthode due au schéma numérique et les erreurs d'arrondi dues aux calculs en virgule flottante. Nous spécifions formellement en Coq le schéma numérique, nous prouvons les deux types d'erreur et nous dérivons une majoration de l'erreur totale. Cela prouve l'adéquation du programme C avec le schéma numérique et la convergence des calculs effectifs. À notre connaissance, c'est la première fois qu'un programme d'analyse numérique est complètement vérifié mécaniquement.
%2 F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs, G.: Mathematics of Computing/G.1: NUMERICAL ANALYSIS/G.1.8: Partial Differential Equations/G.1.8.2: Finite difference methods
%G Anglais
%2 Rapport de recherche
%P 30
%8 2011-12-07
%K Formal proof of numerical program; Convergence of numerical scheme; Proof of C program; Coq formal proof; Acoustic wave equation; Partial differential equation; Rounding error analysis
%Z RR-7826

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="report"><head>Rapports</head>
<biblStruct type="report" xml:id="hal-00649240"><monogr>
<author><persName><forename>Sylvie</forename><surname>Boldo</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Saclay - Ile de France</orgName>
<orgName type="team">PROVAL</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Université Paris XI - Paris Sud</orgName>
<orgName type="institution">CNRS : UMR</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">LRI</orgName>
<orgName type="team">Laboratoire de Recherche en Informatique</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR8623</orgName>
<orgName type="institution">Université Paris XI - Paris Sud</orgName>
</affiliation>
</author>
<author><persName><forename>Francois</forename><surname>Clement</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Paris-Rocquencourt</orgName>
<orgName type="team">ESTIME</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
</affiliation>
</author>
<author><persName><forename>Jean-Christophe</forename><surname>Filliâtre</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Saclay - Ile de France</orgName>
<orgName type="team">PROVAL</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Université Paris XI - Paris Sud</orgName>
<orgName type="institution">CNRS : UMR</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">LRI</orgName>
<orgName type="team">Laboratoire de Recherche en Informatique</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR8623</orgName>
<orgName type="institution">Université Paris XI - Paris Sud</orgName>
</affiliation>
</author>
<author><persName><forename>Micaela</forename><surname>Mayero</surname></persName>
<affiliation>
<orgName type="laboratory">LIPN</orgName>
<orgName type="team">Laboratoire d'informatique de Paris-nord</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR7030</orgName>
<orgName type="institution">Université Paris XIII - Paris Nord</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">Inria Grenoble Rhône-Alpes / LIP Laboratoire de l'Informatique du Parallélisme</orgName>
<orgName type="team">ARENAIRE</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR5668</orgName>
<orgName type="institution">Université Claude Bernard - Lyon I</orgName>
<orgName type="institution">École Normale Supérieure - Lyon</orgName>
</affiliation>
</author>
<author><persName><forename>Guillaume</forename><surname>Melquiond</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Saclay - Ile de France</orgName>
<orgName type="team">PROVAL</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Université Paris XI - Paris Sud</orgName>
<orgName type="institution">CNRS : UMR</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">LRI</orgName>
<orgName type="team">Laboratoire de Recherche en Informatique</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR8623</orgName>
<orgName type="institution">Université Paris XI - Paris Sud</orgName>
</affiliation>
</author>
<author><persName><forename>Pierre</forename><surname>Weis</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Paris-Rocquencourt</orgName>
<orgName type="team">ESTIME</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
</affiliation>
</author>
<title type="main" level="m">Wave Equation Numerical Resolution: Mathematics and Program</title><title type="main" level="m">Wave Equation Numerical Resolution: Mathematics and Program</title><imprint><biblScope type="publicationDate">2011-12-07</biblScope><biblScope type="pp">30</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/hal-00649240</idno><idno type="HALFile">http://hal.inria.fr/hal-00649240/PDF/RR-7826.pdf</idno></biblStruct>
</listBibl>
</listBibl>