Computing differential invariants of hybrid systems as fixedpoints

@ARTICLE{DBLP:journals/fmsd/PlatzerC09,
	pdf = {pub/cdifp.pdf},
	ref = {DBLP:conf/cav/PlatzerC08},
	refname = {CAV'08},
	study = {pub/cdifp-examples.zip},

  author    = {Andr{\'e} Platzer and Edmund M. Clarke},
  title     = {Computing Differential Invariants of Hybrid
               Systems as Fixedpoints},
  journal   = {Form. Methods Syst. Des.},
  longjournal = {Formal Methods in System Design},
  year      = {2009},
  volume    = {35},
  number    = {1},
  pages     = {98-120},
  doi       = {10.1007/s10703-009-0079-8},
  keywords  = {verification of hybrid systems,
               differential invariants, verification logic,
               fixedpoint engine},
  abstract  = {
    We introduce a fixedpoint algorithm for verifying
    safety properties of hybrid systems with differential
    equations whose right-hand sides are polynomials in the
    state variables. In order to verify nontrivial systems
    without solving their differential equations and
    without numerical errors, we use a continuous
    generalization of induction, for which our algorithm
    computes the required differential invariants. As a
    means for combining local differential invariants into
    global system invariants in a sound way, our fixedpoint
    algorithm works with a compositional verification logic
    for hybrid systems. With this compositional approach we
    exploit locality in system designs. To improve the
    verification power, we further introduce a saturation
    procedure that refines the system dynamics successively
    with differential invariants until safety becomes
    provable. By complementing our symbolic verification
    algorithm with a robust version of numerical
    falsification, we obtain a fast and sound verification
    procedure. We verify roundabout maneuvers in air
    traffic management and collision avoidance in train
    control and car control.}
}```