Investigation and Implementation of Invariant Generation in The KeYmaera System for Hybrid
Program invariants are critical for the successful verification of most non-trivial programs. Unfortunately, the generation of invariants is also difficult; this is especially true in the hybrid dynamical systems domain, where future states rarely can be computed exactly. We will overview some techniques for invariant generation in hybrid dynamical systems and their implementation for use in the KeYmaera X theorem prover. We will discuss previous approaches used in KeYmaera, some approaches used by others for invariant generation, and some novel approaches to the invariant generation problem in hybrid dynamical systems.