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 (dL), which is a first-order dynamic logic for hybrid programs, a program notation for hybrid systems. KeYmaera also supports hybrid systems with nonlinear discrete jumps, nonlinear differential equations, differential-algebraic equations, differential inequalities, and systems with nondeterministic discrete or continuous input.
For automation, KeYmaera implements a free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically. This compositional verification principle helps scaling up verification, because KeYmaera verifies a big system by verifying properties of subsystems. To overcome the complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy. The KeYmaera verification tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying case studies from train control, car control, air traffic control, robotics.
The KeYmaera verification tool provides significant automation (up to 100%). It handles differential equations, integrates full first-order real arithmetic and implements differential invariants. KeYmaera implements procedures for automatically generating invariants and differential invariants, but also allows you to specify invariants interactively whenever your case study is too complex for KeYmaera's current automation. The graphical user interface of KeYmaera can be used to navigate and manipulate the proofs discovered by KeYmaera or find more efficient proofs.
Webstart version : http://symbolaris.com/info/KeYmaera.html
Download site : http://symbolaris.com/info/KeYmaera-download.html
Version : 3.0
Last updated : Sep 22, 2012
Date added : November 5, 2007
Directly from KeYmaera website : http://symbolaris.com/info/KeYmaera-guide.html
Directly from KeYmaera website : http://symbolaris.com/info/KeYmaera.html#download
Directly from KeYmaera website : http://symbolaris.com/info/KeYmaera.html#publications
André Platzer, Carnegie Mellon University, Pittsburgh, PA, USA
Jan-David Quesel, University of Oldenburg, Germany
Philipp Rümmer, Uppsala University, Sweden