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

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)

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)

• 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
• Affine systems of ODEs in Isabelle/HOL for hybrid-program verification
• scientific article; zbMATH DE number 65714 (Why is no real title available?)
• 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!

Describes a project that uses

Uses Software

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

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)