Formally-verified round-off error analysis of Runge-Kutta methods
From MaRDI portal
Cites work
- scientific article; zbMATH DE number 3853573 (Why is no real title available?)
- scientific article; zbMATH DE number 733519 (Why is no real title available?)
- scientific article; zbMATH DE number 940566 (Why is no real title available?)
- scientific article; zbMATH DE number 822685 (Why is no real title available?)
- scientific article; zbMATH DE number 3250158 (Why is no real title available?)
- scientific article; zbMATH DE number 3273462 (Why is no real title available?)
- scientific article; zbMATH DE number 961607 (Why is no real title available?)
- A rigorous ODE solver and Smale's 14th problem
- A verified ODE solver and the Lorenz attractor
- Accuracy and Stability of Numerical Algorithms
- Achieving Brouwer's law with implicit Runge-Kutta methods
- C-language floating-point proofs layered with VST and Flocq
- Canonical Big Operators
- Certification of bounds on expressions involving rounded operators
- Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
- Coquelicot: a user-friendly library of real analysis for Coq
- Estimating local truncation errors for Runge-Kutta methods
- Finite element modeling of blood in arteries
- Floats and Ropes: A Case Study for Formal Numerical Program Verification
- Formal proof of a wave equation resolution scheme: the method error
- Formal proofs for theoretical properties of Newton's method
- Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
- Formal verification of a floating-point expansion renormalization algorithm
- Formalization techniques for asymptotic reasoning in classical analysis
- Formally verified approximations of definite integrals
- Formally verified approximations of definite integrals
- Formally verified conditions for regularity of interval matrices
- Functions of Matrices
- Handbook of Floating-Point Arithmetic
- Improved error bounds for floating-point products and Horner's scheme
- MPFR
- Multiple-Precision Correctly rounded Newton-Cotes quadrature
- Nineteen Dubious Ways to Compute the Exponential of a Matrix
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
- Numerical analysis and differential equations
- Numerical methods in astrophysics. An introduction. With CD-ROM.
- On relative errors of floating-point operations: optimal bounds and applications
- Proving Bounds on Real-Valued Functions with Computations
- Round-Off Error and Exceptional Behavior Analysis of Explicit Runge-Kutta Methods
- Round-off error in long-term orbital integrations using multistep methods
- Solving Ordinary Differential Equations I
- Static analysis of finite precision computations
- The Complete Proof Theory of Hybrid Systems
- The flow of ODEs
- Validated computation of the local truncation error of Runge-Kutta methods with automatic differentiation
- Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models
- Verified software toolchain (invited talk)
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
This page was built for publication: Formally-verified round-off error analysis of Runge-Kutta methods
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6149594)
