Wave equation numerical resolution: a comprehensive mechanized proof of a C program
From MaRDI portal
Publication:352952
DOI10.1007/S10817-012-9255-4zbMATH Open1267.68208arXiv1112.1795OpenAlexW2147177731MaRDI QIDQ352952FDOQ352952
Authors: Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis 
Publication date: 5 July 2013
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Abstract: 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.
Full work available at URL: https://arxiv.org/abs/1112.1795
Recommendations
- Formal proof of a wave equation resolution scheme: the method error
- Trusting computations: a mechanized proof from partial differential equations to actual program
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- C-language floating-point proofs layered with VST and Flocq
- Floats and Ropes: A Case Study for Formal Numerical Program Verification
partial differential equationrounding error analysisacoustic wave equationconvergence of numerical schemeCoq formal proofformal proof of numerical programproof of C program
Roundoff error (65G50) Wave equation (35L05) Numerical solution of discretized equations for initial value and initial-boundary value problems involving PDEs (65M22)
Cites Work
- Certification of bounds on expressions involving rounded operators
- Programming Languages and Systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- On the Partial Difference Equations of Mathematical Physics
- Title not available (Why is that?)
- Title not available (Why is that?)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Canonical Big Operators
- Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
- Title not available (Why is that?)
- Title not available (Why is that?)
- Propagation of round-off errors and the role of stability in numerical methods for linear and nonlinear PDEs
- \({\mathcal L}\)-convergence paradox in numerical methods for PDEs
- Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
- A decision procedure for linear ``big O equations
- Title not available (Why is that?)
- \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
- Hilbert's ‘Verunglückter Beweis’, the first epsilon theorem, and consistency proofs
- Proof-irrelevant model of CC with predicative induction and judgmental equality
- Certified Exact Transcendental Real Number Computation in Coq
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Floats and Ropes: A Case Study for Formal Numerical Program Verification
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Type classes for efficient exact real arithmetic in \textsc{Coq}
- Theorem Proving in Higher Order Logics
- Certain Rational Functions Whose Power Series Have Positive Coefficients
- Formal proof of a wave equation resolution scheme: the method error
- Title not available (Why is that?)
- Nonstandard analysis in ACL2
- A comprehensive framework for verification, validation, and uncertainty quantification in scientific computing
- A computer-verified monadic functional implementation of the integral
Cited In (24)
- Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms
- A Coq formalization of Lebesgue integration of nonnegative functions
- Formal analysis of the compact position reporting algorithm
- A formally verified floating-point implementation of the compact position reporting algorithm
- Formally-verified round-off error analysis of Runge-Kutta methods
- Lyapunov functions for linear damped wave equations in one-dimensional space with dynamic boundary conditions
- The flow of ODEs: formalization of variational equation and Poincaré map
- A two-phase approach for conditional floating-point verification
- Deductive verification of floating-point Java programs in KeY
- Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
- Rounding error analysis of linear recurrences using generating series
- Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms
- Affine arithmetic and applications to real-number proving
- Trusting computations: a mechanized proof from partial differential equations to actual program
- A verified ODE solver and the Lorenz attractor
- Quantitative continuity and Computable Analysis in Coq
- Computer-assisted verification of four interval arithmetic operators
- A Coq formalization of Lebesgue induction principle and Tonelli's theorem
- Formalization of real analysis: a survey of proof assistants and libraries
- Provably correct floating-point implementation of a point-in-polygon algorithm
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method
- Coquelicot: a user-friendly library of real analysis for Coq
- Formal proof of a wave equation resolution scheme: the method error
Uses Software
This page was built for publication: Wave equation numerical resolution: a comprehensive mechanized proof of a C program
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q352952)
