Real world verification

@INPROCEEDINGS{DBLP:conf/cade/PlatzerQR09,
	pdf = {pub/rwv.pdf},
	slides = {pub/rwv-slides.pdf},
	study = {pub/rwv-examples.zip},
	TR = {DBLP:conf/cade/PlatzerQR09:TR},

  author    = {Andr{\'e} Platzer and
               Jan-David Quesel and
               Philipp R{\"u}mmer},
  title     = {Real World Verification},
  booktitle = {CADE},
  longbooktitle = {International Conference on Automated
               Deduction, {CADE-22}, Montreal, Canada,
               Proceedings},
  year      = {2009},
  pages     = {485-501},
  editor    = {Renate A. Schmidt},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5663},
  doi       = {10.1007/978-3-642-02959-2_35},
  keywords  = {real-closed fields, decision procedures,
               hybrid systems, software verification},
  abstract  = {
    Scalable handling of real arithmetic is a crucial part
    of the verification of hybrid systems, mathematical
    algorithms, and mixed analog/digital circuits. Despite
    substantial advances in verification technology,
    complexity issues with classical decision procedures
    are still a major obstacle for formal verification of
    real-world applications, e.g., in automotive and
    avionic industries. To identify strengths and
    weaknesses, we examine state of the art symbolic
    techniques and implementations for the universal
    fragment of real-closed fields: approaches based on
    quantifier elimination, Gr\"obner Bases, and
    semidefinite programming for the Positivstellensatz.
    Within a uniform context of the verification tool
    KeYmaera, we compare these approaches qualitatively and
    quantitatively on verification benchmarks from hybrid
    systems, textbook algorithms, and on geometric
    problems. Finally, we introduce a new decision
    procedure combining Gr\"obner Bases and semidefinite
    programming for the real Nullstellensatz that
    outperforms the individual approaches on an interesting
    set of problems.}
}```