Ordinary Differential Equations
Ordinary Differential Equations. Session Ordinary-Differential-Equations formalizes ordinary differential equations (ODEs) and initial value problems. This work comprises proofs for local and global existence of unique solutions (Picard-Lindelöf theorem). Moreover, it contains a formalization of the (continuous or even differentiable) dependency of the flow on initial conditions as the flow of ODEs.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Huerta y Munive, Jonathan Julián; Struth, Georg: Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL (2022)
- Immler, Fabian; Traut, Christoph: The flow of ODEs: formalization of variational equation and Poincaré map (2019)
- Immler, Fabian: A verified ODE solver and the Lorenz attractor (2018)
- Immler, Fabian: A verified enclosure for the Lorenz attractor (rough diamond) (2015)
- Immler, Fabian; Hölzl, Johannes: Numerical analysis of ordinary differential equations in Isabelle/HOL (2012)