Einzeltreffer — DigiBib

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.

Titel:	Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program
Autor/in / Beteiligte Person:	BOLDO, Sylvie ; CLEMENT, François ; FILLIATRE, Jean-Christophe ; MAYERO, Micaela ; MELQUIOND, Guillaume ; WEIS, Pierre
Link:	Full Text Finder (Volltext) E-Journal im Bestand der UB Hagen? View record from PASCAL Archive
Zeitschrift:	Journal of automated reasoning, Jg. 50 (2013), Heft 4, S. 423-456
Veröffentlichung:	Heidelberg: Springer, 2013
Medientyp:	academicJournal
Umfang:	print, 58 ref
ISSN:	0168-7433 (print)
Schlagwort:	Cognition Computer science Informatique Sciences exactes et technologie Exact sciences and technology Sciences et techniques communes Sciences and techniques of general use Mathematiques Mathematics Logique mathématique, fondements, théorie des ensembles Mathematical logic, foundations, set theory Logique et fondements Logic and foundations Théorie de la preuve et mathématiques constructives Proof theory and constructive mathematics Physique Physics Domaines classiques de la physique (y compris les applications) Fundamental areas of phenomenology (including applications) Acoustique Acoustics Acoustique linéaire Linear acoustics Sciences appliquees Applied sciences Informatique; automatique theorique; systemes Computer science; control theory; systems Logiciel Software Performances des systèmes informatiques. Fiabilité Computer systems performance. Reliability Analyse temporelle Time analysis Análisis temporal Calcul erreur Error analysis Cálculo error Consistance sémantique Soundness Consistencia semantica Equation dérivée partielle Partial differential equation Ecuación derivada parcial Equation onde Wave equation Ecuación onda Erreur arrondi Rounding error Error redondear Erreur bornée Bounded error Error acotada Estimation erreur Error estimation Estimación error Modélisation Modeling Modelización Méthode formelle Formal method Método formal Onde acoustique Acoustic wave Onda acústica Satisfiabilité Satisfiability Satisfactibilidad Théorie preuve Proof theory Teoría demonstración Virgule flottante Floating point Coma flotante Vérification programme Program verification Verificación programa Vérification formelle Formal verification Verificación formal Acoustic wave equation Convergence of numerical scheme Coq formal proof Formal proof of numerical program Proof of C program Rounding error analysis
Sonstiges:	Nachgewiesen in: PASCAL Archive Sprachen: English Original Material: INIST-CNRS Document Type: Article File Description: text Language: English Author Affiliations: ProVal, INRIA Saclay ― Île-de-France, Orsay 91893, France ; LRI, UMR 8623, Université Paris-Sud, CNRS, Orsay 91405, France ; Pomdapi, INRIA Paris - Rocquencourt, Le Chesnay 78153, France ; LIPN, UMR 7030, Université de Paris-Nord, CNRS, Villetaneuse, 93430, France ; LIP, Arénaire (INRIA Grenoble - Rhône-Alpes, CNRS UMR 5668, UCBL, ENS Lyon), Lyon, 69364, France Rights: Copyright 2015 INIST-CNRS ; CC BY 4.0 ; Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS Notes: Computer science; theoretical automation; systems ; Mathematics ; Physics: acoustics

Klicken Sie ein Format an und speichern Sie dann die Daten oder geben Sie eine Empfänger-Adresse ein und lassen Sie sich per Email zusenden.

BibTeX Citavi, JabRef, u.a.
(Literaturverwaltung)

PDF kein Volltext!
(Merkzettel, Notizen)

RIS Endnote, Citavi u.a.
(Literaturverwaltung)

MODS
(XML zur Weiterverarbeitung)

oder

Wählen Sie das für Sie passende Zitationsformat und kopieren Sie es dann in die Zwischenablage, lassen es sich per Mail zusenden oder speichern es als PDF-Datei.

Gewünschter Zitations-Stil:

oder

Bitte prüfen Sie, ob die Zitation formal korrekt ist, bevor Sie sie in einer Arbeit verwenden. Benutzen Sie gegebenenfalls den "Exportieren"-Dialog, wenn Sie ein Literaturverwaltungsprogramm verwenden und die Zitat-Angaben selbst formatieren wollen.

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