Formal Proof of a Wave Equation Resolution Scheme: The Method Error

DOI10.1007/978-3-642-14052-5_12zbMath1291.68329arXiv1005.0824OpenAlexW3103675537MaRDI QIDQ5747647

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

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

partial differential equationacoustic wave equationnumerical schemeCoq formal proofs

Mathematics Subject Classification ID

Related Items (9)

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

Uses Software

• ACL2
• Coq
• Isabelle/HOL
• PVS

This page was built for publication: Formal Proof of a Wave Equation Resolution Scheme: The Method Error