HAL - INRIA :: [hal-00649240, version 2] Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program

hal-00649240, version 2

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

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

N° RR-7826 (2011)

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

a – INRIA
b – CNRS
c – Université Paris-Nord - Paris XIII
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

hal-00649240, version 2
http://hal.inria.fr/hal-00649240
oai:hal.inria.fr:hal-00649240
Contributeur : Francois Clement <>
Soumis le : Mardi 15 Mai 2012, 16:12:27
Dernière modification le : Mercredi 16 Mai 2012, 08:57:14

Voir la fiche détaillée

Documents associés

PDF :

PS :

arXiv : 1112.1795

Exporter

Bibtex EndNote TEI RefWorks

%F hal-00649240, version 2
%0 Report
%U http://hal.inria.fr/hal-00649240
%2 INFO:INFO_LO;MATH:MATH_NA
%T Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C 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 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 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.
%2 Nous prouvons formellement la correction d'un programme C implémentant un schéma numérique 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 l'erreur d'arrondi due aux calculs en virgule flottante. Nous annotons ce programme C pour spécifier ces deux types d'erreur. Nous utilisons Frama-C pour générer les théorèmes qui garantissent la correction du code. Nous prouvons ces théorèmes à l'aide de solveurs SMT, de Gappa et de Coq. Un développement Coq important est nécessaire pour prouver l'adéquation du programme C au schéma numérique et pour borner les erreurs. À notre connaissance, c'est la première fois qu'un tel 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 32
%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 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="m">Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program</title><title type="main" level="m">Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program</title><imprint><biblScope type="publicationDate">2011-12-07</biblScope><biblScope type="pp">32</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>