  This article presents an axiomatic approach for deductive verification of
existence and liveness for ordinary differential equations (ODEs) with
differential dynamic logic (dL). The approach yields proofs that the solution
of a given ODE exists long enough to reach a given target region without
leaving a given evolution domain. Numerous subtleties complicate the
generalization of discrete liveness verification techniques, such as loop
variants, to the continuous setting. For example, ODE solutions may blow up in
finite time or their progress towards the goal may converge to zero. These
subtleties are handled in dL by successively refining ODE liveness properties
using ODE invariance properties which have a complete axiomatization. This
approach is widely applicable: several liveness arguments from the literature
are surveyed and derived as special instances of axiomatic refinement in dL.
These derivations also correct several soundness errors in the surveyed
literature, which further highlights the subtlety of ODE liveness reasoning and
the utility of an axiomatic approach. An important special case of this
approach deduces (global) existence properties of ODEs, which are a fundamental
part of every ODE liveness argument. Thus, all generalizations of existence
properties and their proofs immediately lead to corresponding generalizations
of ODE liveness arguments. Overall, the resulting library of common refinement
steps enables both the sound development and justification of new ODE existence
and of liveness proof rules from dL axioms. These insights are put into
practice through an implementation of ODE liveness proofs in the KeYmaera X
theorem prover for hybrid systems.
