KeYmaera: A Hybrid Theorem Prover for Hybrid Systems ?
Jan-David Quesel · 2008
KeYmaera is a hybrid verication tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a nat- ural specication and verication logic for hybrid systems. KeYmaera supports dierential dynamic logic , which is a real-valued rst-order dynamic logic for hybrid programs, a program notation for hybrid au- tomata. For automating the verication process, KeYmaera implements a generalized free-variable sequent calculus and automatic proof strate- gies that decompose the hybrid system specication symbolically. To overcome the complexity of real arithmetic, we integrate real quantier 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 trac management.