Computing differential invariants of hybrid systems as fixedpoints

@INPROCEEDINGS{DBLP:conf/cav/PlatzerC08,
	pdf = {pub/fpdi.pdf},
	slides = {pub/fpdi-slides.pdf},
	ref = {DBLP:journals/fmsd/PlatzerC09},
	refname = {FMSD'09},
	study = {pub/fpdi-examples.zip},
	TR = {DBLP:conf/cav/PlatzerC08:TR},

  author    = {Andr{\'e} Platzer and
               Edmund M. Clarke},
  title     = {Computing Differential Invariants of Hybrid
               Systems as Fixedpoints},
  booktitle = {CAV},
  longbooktitle = {Computer Aided Verification, 20th
               International Conference, CAV 2008,
               Princeton, NJ, USA, July 7-14, 2008,
               Proceedings},
  year      = {2008},
  pages     = {176-189},
  month     = {},
  editor    = {Aarti Gupta and
               Sharad Malik},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5123},
  isbn      = {978-3-540-70543-7},
  doi       = {10.1007/978-3-540-70545-1_17},
  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. 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.}
}```