Formally-verified round-off error analysis of Runge-Kutta methods
From MaRDI portal
Publication:6149594
DOI10.1007/s10817-023-09686-yOpenAlexW4389381430MaRDI QIDQ6149594
Publication date: 6 February 2024
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-023-09686-y
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Improved error bounds for floating-point products and Horner's scheme
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Estimating local truncation errors for Runge-Kutta methods
- Achieving Brouwer's law with implicit Runge-Kutta methods
- Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models
- A rigorous ODE solver and Smale's 14th problem
- A verified ODE solver and the Lorenz attractor
- Formal verification of a floating-point expansion renormalization algorithm
- Formally verified approximations of definite integrals
- Finite element modeling of blood in arteries
- Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
- Coquelicot: a user-friendly library of real analysis for Coq
- Round-off error in long-term orbital integrations using multistep methods
- The Flow of ODEs
- Formally Verified Approximations of Definite Integrals
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
- The Complete Proof Theory of Hybrid Systems
- Certification of bounds on expressions involving rounded operators
- Verified Software Toolchain
- Static Analysis of Finite Precision Computations
- Formal proofs for theoretical properties of Newton's method
- Solving Ordinary Differential Equations I
- Proving Bounds on Real-Valued Functions with Computations
- Canonical Big Operators
- MPFR
- Formally Verified Conditions for Regularity of Interval Matrices
- Handbook of Floating-Point Arithmetic
- Floats and Ropes: A Case Study for Formal Numerical Program Verification
- Nineteen Dubious Ways to Compute the Exponential of a Matrix
- On relative errors of floating-point operations: Optimal bounds and applications
- Validated computation of the local truncation error of Runge–Kutta methods with automatic differentiation
- Accuracy and Stability of Numerical Algorithms
- C-language floating-point proofs layered with VST and Flocq
- Round-Off Error and Exceptional Behavior Analysis of Explicit Runge-Kutta Methods
- Multiple-Precision Correctly rounded Newton-Cotes quadrature
- Functions of Matrices
- Formal Proof of a Wave Equation Resolution Scheme: The Method Error
This page was built for publication: Formally-verified round-off error analysis of Runge-Kutta methods
