The flow of ODEs
DOI10.1007/978-3-319-43144-4_12zbMATH Open1468.68324OpenAlexW2483648716MaRDI QIDQ2829258FDOQ2829258
Authors: Fabian Immler, Christoph Traut 
Publication date: 27 October 2016
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-43144-4_12
Recommendations
- The flow of ODEs: formalization of variational equation and Poincaré map
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
- Affine systems of ODEs in Isabelle/HOL for hybrid-program verification
- Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models
- scientific article; zbMATH DE number 1273683
Initial value problems, existence, uniqueness, continuous dependence and continuation of solutions to ordinary differential equations (34A12) Geometric methods in ordinary differential equations (34A26) Dynamics induced by flows and semiflows (37C10) Mechanization of proofs and logical operations (03B35) Numerical methods for initial value problems involving ordinary differential equations (65L05) Formalization of mathematics in connection with theorem provers (68V20)
Cites Work
- A rigorous ODE solver and Smale's 14th problem
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Isabelle/HOL. A proof assistant for higher-order logic
- Type classes and filters for mathematical analysis in Isabelle/HOL
- Differential equations, dynamical systems, and an introduction to chaos
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
Cited In (11)
- A Coq formalization of Lebesgue integration of nonnegative functions
- Formally-verified round-off error analysis of Runge-Kutta methods
- The flow of ODEs: formalization of variational equation and Poincaré map
- Title not available (Why is that?)
- Ode to the PST
- A verified ODE solver and the Lorenz attractor
- A formally verified proof of the central limit theorem
- Verified interactive computation of definite integrals
- From ODE to DDE
- Bellerophon: tactical theorem proving for hybrid systems
- Give your ODEs a singular perturbation!
Uses Software
This page was built for publication: The flow of ODEs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829258)
