Ordinary Differential Equations

Fabian Immler 🌐 and Johannes Hölzl 🌐

April 26, 2012

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.

Not in the generated document are the following sessions:

  • HOL-ODE-Numerics: Rigorous numerical algorithms for computing enclosures of solutions based on Runge-Kutta methods and affine arithmetic. Reachability analysis with splitting and reduction at hyperplanes.
  • HOL-ODE-Examples: Applications of the numerical algorithms to concrete systems of ODEs.
  • Lorenz_C0, Lorenz_C1: Verified algorithms for checking C1-information according to Tucker's proof, computation of C0-information.


BSD License


September 20, 2017
added Poincare map and propagation of variational equation in reachability analysis, verified algorithms for C1-information and computations for C0-information of the Lorenz attractor.
August 3, 2016
numerical algorithms for reachability analysis (using second-order Runge-Kutta methods, splitting, and reduction) implemented using Lammich's framework for automatic refinement
April 14, 2016
added flow and variational equation
February 13, 2014
added an implementation of the Euler method based on affine arithmetic


Session Ordinary_Differential_Equations

Session HOL-ODE-Numerics

Session Lorenz_Approximation

Session HOL-ODE-Examples


Session Lorenz_C0

Session Lorenz_C1