Wave equation numerical resolution: a comprehensive mechanized proof of a C program
From MaRDI portal
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.
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
Cites work
- scientific article; zbMATH DE number 1670741 (Why is no real title available?)
- scientific article; zbMATH DE number 1231230 (Why is no real title available?)
- scientific article; zbMATH DE number 1237702 (Why is no real title available?)
- scientific article; zbMATH DE number 1259143 (Why is no real title available?)
- scientific article; zbMATH DE number 529531 (Why is no real title available?)
- scientific article; zbMATH DE number 2003158 (Why is no real title available?)
- scientific article; zbMATH DE number 1927426 (Why is no real title available?)
- scientific article; zbMATH DE number 2085168 (Why is no real title available?)
- scientific article; zbMATH DE number 1863384 (Why is no real title available?)
- scientific article; zbMATH DE number 815352 (Why is no real title available?)
- scientific article; zbMATH DE number 3423635 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- scientific article; zbMATH DE number 3078450 (Why is no real title available?)
- A comprehensive framework for verification, validation, and uncertainty quantification in scientific computing
- A computer-verified monadic functional implementation of the integral
- A decision procedure for linear ``big O equations
- Canonical Big Operators
- Certain Rational Functions Whose Power Series Have Positive Coefficients
- Certification of bounds on expressions involving rounded operators
- Certified Exact Transcendental Real Number Computation in Coq
- Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
- Floats and Ropes: A Case Study for Formal Numerical Program Verification
- Formal proof of a wave equation resolution scheme: the method error
- Hilbert's ‘Verunglückter Beweis’, the first epsilon theorem, and consistency proofs
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Nonstandard analysis in ACL2
- On the Partial Difference Equations of Mathematical Physics
- Programming Languages and Systems
- Proof-irrelevant model of CC with predicative induction and judgmental equality
- Propagation of round-off errors and the role of stability in numerical methods for linear and nonlinear PDEs
- Theorem Proving in Higher Order Logics
- Type classes for efficient exact real arithmetic in \textsc{Coq}
- \({\mathcal L}\)-convergence paradox in numerical methods for PDEs
- \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
Cited in
(24)- Formalization of real analysis: a survey of proof assistants and libraries
- Formally-verified round-off error analysis of Runge-Kutta methods
- A two-phase approach for conditional floating-point verification
- Deductive verification of floating-point Java programs in KeY
- Trusting computations: a mechanized proof from partial differential equations to actual program
- Rounding error analysis of linear recurrences using generating series
- A verified ODE solver and the Lorenz attractor
- A formally verified floating-point implementation of the compact position reporting algorithm
- Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms
- A Coq formalization of Lebesgue integration of nonnegative functions
- Provably correct floating-point implementation of a point-in-polygon algorithm
- Coquelicot: a user-friendly library of real analysis for Coq
- Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
- 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
- Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms
- Affine arithmetic and applications to real-number proving
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- Formal proof of a wave equation resolution scheme: the method error
- Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method
- 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
- Formal analysis of the compact position reporting algorithm
Describes a project that uses
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)
