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

numerical schemepartial differential equationacoustic wave equationCoq formal proofs

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

(10)

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

Describes a project that uses

Uses Software

• PVS
• Isabelle/HOL
• Coq
• ACL2

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)