@inproceedings{DBLP:conf/cade/PlatzerQ08,
pdf = {pub/KeYmaera.pdf},
slides = {pub/KeYmaera-slides.pdf},
author = {['André Platzer', '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', 'Peter Baumgartner', '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.}
}