Trusting computations: a mechanized proof from partial differential equations to actual program

DOI10.1016/j.camwa.2014.06.004zbMath1369.35051arXiv1212.6641OpenAlexW2013562423MaRDI QIDQ2398899

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

Publication date: 21 August 2017

Published in: Computers \& Mathematics with Applications (Search for Journal in Brave)

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

zbMATH Keywords

acoustic wave equationconvergence of numerical schemerounding error analysisformal proof of numerical program

Mathematics Subject Classification ID

Related Items (10)

Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B ⋮ Event-B refinement for continuous behaviours approximation ⋮ Affine Arithmetic and Applications to Real-Number Proving ⋮ A Coq formalization of Lebesgue integration of nonnegative functions ⋮ Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method ⋮ On the formalization of the heat conduction problem in HOL ⋮ Rounding error analysis of linear recurrences using generating series ⋮ Unnamed Item ⋮ Automatic pre- and postconditions for partial differential equations ⋮ On the Coalgebra of Partial Differential Equations

Uses Software

• Coq
• KRAKATOA
• ACSL
• Why3
• Caduceus
• Gappa
• cvc3
• z3
• Flocq
• seL4

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A fast algorithm for proving terminating hypergeometric identities
• The method of creative telescoping
• Adaptive Inexact Newton Methods with A Posteriori Stopping Criteria for Nonlinear Diffusion PDEs
• CC(X): Semantic Combination of Congruence Closure with Solvable Theories
• Certification of bounds on expressions involving rounded operators
• Canonical Big Operators
• Combining Coq and Gappa for Certifying Floating-Point Programs
• Floats and Ropes: A Case Study for Formal Numerical Program Verification
• Guarded commands, nondeterminacy and formal derivation of programs
• Positive Sums of the Classical Orthogonal Polynomials
• Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
• Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
• On the Partial Difference Equations of Mathematical Physics
• Certain Rational Functions Whose Power Series Have Positive Coefficients
• Formal Proof of a Wave Equation Resolution Scheme: The Method Error

This page was built for publication: Trusting computations: a mechanized proof from partial differential equations to actual program