The flow of ODEs: formalization of variational equation and Poincaré map

DOI10.1007/s10817-018-9449-5zbMath1468.68325OpenAlexW2793741686MaRDI QIDQ1722644

Fabian Immler, Christoph Traut

Publication date: 18 February 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-018-9449-5

zbMATH Keywords

ordinary differential equationdynamical systemPoincaré mapIsabelle/HOL

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

Related Items (4)

Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL ⋮ Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method ⋮ On the formalization of the heat conduction problem in HOL

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• HOL
• Coquelicot
• Transfer
• Lifting
• Ergodic theory
• Lp spaces
• Archive Formal Proofs
• Ordinary Differential Equations
• RODES

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• A formalization of metric spaces in HOL Light
• Isabelle/HOL. A proof assistant for higher-order logic
• A rigorous ODE solver and Smale's 14th problem
• The HOL Light theory of Euclidean space
• Coquelicot: a user-friendly library of real analysis for Coq
• The Flow of ODEs
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Formalization of real analysis: a survey of proof assistants and libraries
• Mechanizing Nonstandard Real Analysis
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• The Picard Algorithm for Ordinary Differential Equations in Coq
• Theorem Proving in Higher Order Logics

This page was built for publication: The flow of ODEs: formalization of variational equation and Poincaré map