KeYmaera: A hybrid theorem prover for hybrid systems.

@INPROCEEDINGS{DBLP:conf/cade/PlatzerQ08,
	pdf = {pub/KeYmaera.pdf},
	slides = {pub/KeYmaera-slides.pdf},

  author    = {Andr{\'e} Platzer and
               Jan-David Quesel},
  title     = {{KeYmaera}: A Hybrid Theorem Prover for
               Hybrid Systems.},
  booktitle = {IJCAR},
  longbooktitle = {Automated Reasoning, Fourth
               International Joint Conference, IJCAR 2008,
               Sydney, Australia, Proceedings},
  year      = {2008},
  pages     = {171-178},
  editor    = {Alessandro Armando and
               Peter Baumgartner and
               Gilles Dowek},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5195},
  isbn      = {978-3-540-71069-1},
  issn      = {0302-9743},
  subseries = {LNAI},
  doi       = {10.1007/978-3-540-71070-7_15},
  keywords  = {dynamic logic, automated theorem proving,
               decision procedures, computer algebra,
               verification of hybrid systems},
  abstract  = {
    KeYmaera is a hybrid verification tool for hybrid
    systems that combines deductive, real algebraic, and
    computer algebraic prover technologies. It is an
    automated and interactive theorem prover for a natural
    specification and verification logic for hybrid
    systems. KeYmaera supports differential dynamic logic,
    which is a real-valued first-order dynamic logic for
    hybrid programs, a program notation for hybrid
    automata. For automating the verification process,
    KeYmaera implements a generalized free-variable sequent
    calculus and automatic proof strategies that decompose
    the hybrid system specification symbolically. To
    overcome the complexity of real arithmetic, we
    integrate real quantifier elimination following an
    iterative background closure strategy. Our tool is
    particularly suitable for verifying parametric hybrid
    systems and has been used successfully for verifying
    collision avoidance in case studies from train control
    and air traffic management.}
}```