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

DOI10.1016/J.CAMWA.2014.06.004zbMATH Open1369.35051arXiv1212.6641OpenAlexW2013562423MaRDI QIDQ2398899FDOQ2398899

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

Publication date: 21 August 2017

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

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.

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

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

zbMATH Keywords

rounding error analysisacoustic wave equationconvergence of numerical schemeformal proof of numerical program

Mathematics Subject Classification ID

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)

Cites Work

• Certification of bounds on expressions involving rounded operators
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Verification and validation in scientific computing.
• On the Partial Difference Equations of Mathematical Physics
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Canonical Big Operators
• Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
• Guarded commands, nondeterminacy and formal derivation of programs
• Positive Sums of the Classical Orthogonal Polynomials
• The method of creative telescoping
• A fast algorithm for proving terminating hypergeometric identities
• Adaptive inexact Newton methods with a posteriori stopping criteria for nonlinear diffusion PDEs
• \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Combining Coq and Gappa for Certifying Floating-Point Programs
• Floats and Ropes: A Case Study for Formal Numerical Program Verification
• Title not available (Why is that?)
• Certain Rational Functions Whose Power Series Have Positive Coefficients
• Formal proof of a wave equation resolution scheme: the method error
• Title not available (Why is that?)
• Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives

Cited In (14)

• Event-B refinement for continuous behaviours approximation
• A Coq formalization of Lebesgue integration of nonnegative functions
• On the Coalgebra of Partial Differential Equations
• Verifying properties of differentiable programs
• On the formalization of the heat conduction problem in HOL
• Rounding error analysis of linear recurrences using generating series
• Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B
• Affine arithmetic and applications to real-number proving
• Automatic pre- and postconditions for partial differential equations
• Formal Derivation of a High-Trustworthy Generic Algorithmic Program for Solving a Class of Path Problems
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method
• Title not available (Why is that?)
• Formal proof of a wave equation resolution scheme: the method error

Uses Software

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

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)