HAL - INRIA :: [inria-00450789, version 3] Formal Proof of a Wave Equation Resolution Scheme: the Method Error

inria-00450789, version 3

Formal Proof of a Wave Equation Resolution Scheme: the Method Error

Sylvie Boldo ()^c^, 1, 2, François Clément ( Author to contact preferably )^c^, 3, Jean-Christophe Filliâtre ()^a^, 1, 2, Micaela Mayero ()^b^, 4, 5, Guillaume Melquiond ()^c^, 1, 2, Pierre Weis ()^c^, 3

ITP'10 - Interactive Theorem Proving 6172 (2010) 147-162

Abstract: Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest one and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs. To our knowledge, this is the first time such kind of mathematical proof is 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 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

inria-00450789, version 3
http://hal.inria.fr/inria-00450789
oai:hal.inria.fr:inria-00450789
From: Francois Clement <>
Submitted on: Wednesday, 11 May 2011 17:14:01
Updated on: Tuesday, 29 November 2011 11:54:20

See detailed view

Associated documents

PDF :

PS :

arXiv: 1005.0824

DOI: 10.1007/978-3-642-14052-5_12

Export

Bibtex EndNote TEI RefWorks

%F inria-00450789, version 3
%0 Conference Proceedings
%U http://hal.inria.fr/inria-00450789
%2 INFO:INFO_LO;MATH:MATH_NA
%T Formal Proof of a Wave Equation Resolution Scheme: the Method Error
%A Boldo, Sylvie
%A Clément, François
%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 Rocquencourt , Laboratoire d'informatique de Paris-nord - LIPN , ARENAIRE - Inria Grenoble Rhône-Alpes / LIP Laboratoire de l'Informatique du Parallélisme
%X Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest one and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs. To our knowledge, this is the first time such kind of mathematical proof is machine-checked.
%2 Les schémas numériques de résolution de l'équation des ondes en dimension 1 sont notoirement convergents. Nous présentons une formalisation détaillée du schéma le plus simple et nous prouvons formellement sa convergence dans le système d'aide à la preuve Coq. La difficulté principale se situe dans la définition adéquate des comportements asymptotiques et du fait que ces comportements ne sont pas complètement décrits dans les preuves sur papier. À notre connaissance, c'est la première mécanisation complète d'une telle preuve en analyse numérique.
%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 English
%8 2010-07-11
%2 international
%B ITP'10 - Interactive Theorem Proving
%2 Edinburgh
%2 United Kingdom
%8 2010-07-11
%8 2010-07-14
%E Matt Kaufmann and Lawrence C. Paulson
%I Springer
%2 Interactive Theorem Proving
%V 6172
%N Lecture Notes in Computer Science
%P 147-162
%R 10.1007/978-3-642-14052-5_12
%K partial differential equation;acoustic wave equation;numerical scheme;Coq formal proofs
%2 arXiv:1005.0824

<?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="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="inria-00450789"><analytic>
<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>François</forename><surname>Clément</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA 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 Rocquencourt</orgName>
<orgName type="team">ESTIME</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
</affiliation>
</author>
<title type="main" level="a">Formal Proof of a Wave Equation Resolution Scheme: the Method Error</title></analytic><monogr><meeting>ITP'10 - Interactive Theorem Proving</meeting><imprint><publisher>Springer</publisher><pubPlace><settlement>Edinburgh</settlement><country>United Kingdom</country></pubPlace><biblScope type="publicationDate">2010-07-11</biblScope><biblScope type="vol">6172</biblScope><biblScope type="pp">147-162</biblScope></imprint></monogr><idno type="doi">10.1007/978-3-642-14052-5_12</idno><idno type="HALid">http://hal.inria.fr/inria-00450789</idno><idno type="HALFile">http://hal.inria.fr/inria-00450789/PDF/RR-7181.pdf</idno></biblStruct>
</listBibl>
</listBibl>