Wave equation numerical resolution: a comprehensive mechanized proof of a C program
From MaRDI portal
Publication:352952
DOI10.1007/s10817-012-9255-4zbMath1267.68208arXiv1112.1795OpenAlexW2147177731MaRDI QIDQ352952
Micaela Mayero, Guillaume Melquiond, François Clément, Pierre Weis, Sylvie Boldo, Jean-Christophe Filliâtre
Publication date: 5 July 2013
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1112.1795
partial differential equationacoustic wave equationconvergence of numerical schemerounding error analysisCoq formal proofformal proof of numerical programproof of C program
Wave equation (35L05) Roundoff error (65G50) Numerical solution of discretized equations for initial value and initial-boundary value problems involving PDEs (65M22)
Related Items
Trusting computations: a mechanized proof from partial differential equations to actual program, A verified ODE solver and the Lorenz attractor, Computer-assisted verification of four interval arithmetic operators, Affine Arithmetic and Applications to Real-Number Proving, A Coq formalization of Lebesgue integration of nonnegative functions, Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method, Formally-verified round-off error analysis of Runge-Kutta methods, Rounding error analysis of linear recurrences using generating series, A Coq formalization of Lebesgue induction principle and Tonelli's theorem, Formalization of real analysis: a survey of proof assistants and libraries, Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms, The flow of ODEs: formalization of variational equation and Poincaré map, Quantitative continuity and Computable Analysis in Coq, A two-phase approach for conditional floating-point verification, Deductive verification of floating-point Java programs in KeY, Formal analysis of the compact position reporting algorithm, Coquelicot: a user-friendly library of real analysis for Coq, A formally verified floating-point implementation of the compact position reporting algorithm, Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions, Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A comprehensive framework for verification, validation, and uncertainty quantification in scientific computing
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A computer-verified monadic functional implementation of the integral
- 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
- CC(X): Semantic Combination of Congruence Closure with Solvable Theories
- Certification of bounds on expressions involving rounded operators
- Hilbert's ‘Verunglückter Beweis’, the first epsilon theorem, and consistency proofs
- Proof-irrelevant model of CC with predicative induction and judgmental equality
- Canonical Big Operators
- 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
- Type classes for efficient exact real arithmetic in Coq
- Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
- Programming Languages and Systems
- Theorem Proving in Higher Order Logics
- On the Partial Difference Equations of Mathematical Physics
- Certain Rational Functions Whose Power Series Have Positive Coefficients
- Formal Proof of a Wave Equation Resolution Scheme: The Method Error
- Nonstandard analysis in ACL2
