Trusting computations: a mechanized proof from partial differential equations to actual program
From MaRDI portal
Publication:2398899
rounding error analysisacoustic wave equationconvergence of numerical schemeformal proof of numerical program
PDEs in connection with fluid mechanics (35Q35) Finite difference methods for initial value and initial-boundary value problems involving PDEs (65M06) Stability and convergence of numerical methods for initial value and initial-boundary value problems involving PDEs (65M12) Specification and verification (program logics, model checking, etc.) (68Q60) Algorithms with automatic result verification (65G20)
Abstract: Computer programs may go wrong due to exceptional behaviors, out-of-bound array accesses, or simply coding errors. Thus, they cannot be blindly trusted. Scientific computing programs make no exception in that respect, and even bring specific accuracy issues due to their massive use of floating-point computations. Yet, it is uncommon to guarantee their correctness. Indeed, we had to extend existing methods and tools for proving the correct behavior of programs to verify an existing numerical analysis program. This C program implements the second-order centered finite difference explicit scheme for solving the 1D wave equation. In fact, we have gone much further as we have mechanically verified the convergence of the numerical scheme in order to get a complete formal proof covering all aspects from partial differential equations to actual numerical results. To the best of our knowledge, this is the first time such a comprehensive proof is achieved.
Recommendations
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Floats and Ropes: A Case Study for Formal Numerical Program Verification
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- Formal proof of a wave equation resolution scheme: the method error
- scientific article; zbMATH DE number 3870488
Cites work
- scientific article; zbMATH DE number 43732 (Why is no real title available?)
- scientific article; zbMATH DE number 1231230 (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 872231 (Why is no real title available?)
- scientific article; zbMATH DE number 911319 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- A fast algorithm for proving terminating hypergeometric identities
- Adaptive inexact Newton methods with a posteriori stopping criteria for nonlinear diffusion PDEs
- Canonical Big Operators
- Certain Rational Functions Whose Power Series Have Positive Coefficients
- Certification of bounds on expressions involving rounded operators
- Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Floats and Ropes: A Case Study for Formal Numerical Program Verification
- Formal proof of a wave equation resolution scheme: the method error
- Guarded commands, nondeterminacy and formal derivation of programs
- Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- On the Partial Difference Equations of Mathematical Physics
- Positive Sums of the Classical Orthogonal Polynomials
- The method of creative telescoping
- Verification and validation in scientific computing.
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
Cited in
(14)- Verifying properties of differentiable programs
- Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B
- Rounding error analysis of linear recurrences using generating series
- Formal Derivation of a High-Trustworthy Generic Algorithmic Program for Solving a Class of Path Problems
- A new finite difference scheme for high-dimensional heat equation
- A Coq formalization of Lebesgue integration of nonnegative functions
- On the Coalgebra of Partial Differential Equations
- On the formalization of the heat conduction problem in HOL
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Affine arithmetic and applications to real-number proving
- Event-B refinement for continuous behaviours approximation
- Formal proof of a wave equation resolution scheme: the method error
- Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method
- Automatic pre- and postconditions for partial differential equations
This page was built for publication: Trusting computations: a mechanized proof from partial differential equations to actual program
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2398899)
