Formal proof of a wave equation resolution scheme: the method error

DOI10.1007/978-3-642-14052-5_12MaRDI QIDQ5747647zbMATH OpenOpenAlexFDO

Authors Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis

Publication date 14 September 2010

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1005.0824

zbMATH Keywords

acoustic wave equationCoq formal proofsnumerical schemepartial differential equation

Mathematics Subject Classification ID

Wave equation (35L05) Finite difference methods for initial value and initial-boundary value problems involving PDEs (65M06)

Abstract: Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest one and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs. To our knowledge, this is the first time such kind of mathematical proof is machine-checked.

Recommendations

• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Trusting computations: a mechanized proof from partial differential equations to actual program
• scientific article; zbMATH DE number 1927426
• Numerical resolution of the wave equation using the spectral method
• Study of the numerical solution to the wave equation

Cited in

(11)

• Iterative learning control for boundary tracking of uncertain nonlinear wave equations
• Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
• Trusting computations: a mechanized proof from partial differential equations to actual program
• Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• scientific article; zbMATH DE number 6787519 (Why is no real title available?)
• Formally-verified round-off error analysis of Runge-Kutta methods
• On the formalization of the heat conduction problem in HOL
• Formally verified roundoff error bounds on LogSumExp-based computations

Describes a project that uses

Uses Software

• Isabelle/HOL
• ACL2
• Coq
• PVS

This page was built for publication: Formal proof of a wave equation resolution scheme: the method error

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5747647)