The flow of ODEs

DOI10.1007/978-3-319-43144-4_12MaRDI QIDQ2829258zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) 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) Numerical methods for initial value problems involving ordinary differential equations (65L05) Formalization of mathematics in connection with theorem provers (68V20)

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

Cites work

• A rigorous ODE solver and Smale's 14th problem
• Differential equations, dynamical systems, and an introduction to chaos
• Isabelle/HOL. A proof assistant for higher-order logic
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• Type classes and filters for mathematical analysis in Isabelle/HOL

Cited in

(12)

• From ODE to DDE
• Give your ODEs a singular perturbation!
• A verified ODE solver and the Lorenz attractor
• Bellerophon: tactical theorem proving for hybrid systems
• A formally verified proof of the central limit theorem
• The flow of ODEs: formalization of variational equation and Poincaré map
• Affine systems of ODEs in Isabelle/HOL for hybrid-program verification
• Verified interactive computation of definite integrals
• A Coq formalization of Lebesgue integration of nonnegative functions
• scientific article; zbMATH DE number 65714 (Why is no real title available?)
• Ode to the PST
• Formally-verified round-off error analysis of Runge-Kutta methods

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL
• Transfer
• Lifting
• RODES

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)