KeYmaera: A hybrid theorem prover for hybrid systems. (System description). (English) Zbl 1165.68469

Platzer, André; Quesel, Jan-David

Armando, Alessandro (ed.) et al., Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12–15, 2008 Proceedings. Berlin: Springer (ISBN 978-3-540-71069-1/pbk). Lecture Notes in Computer Science 5195. Lecture Notes in Artificial Intelligence, 171-178 (2008).

Summary: 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.
For the entire collection see [Zbl 1149.68003].

MSC:

68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q60	Specification and verification (program logics, model checking, etc.)

Keywords:

dynamic logic; automated theorem proving; decision procedures; computer algebra; verification of hybrid systems

Software:

KeYmaera; Orbital library; PHAVer; HyTech; QEPCAD