KeYmaera

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.

Downloads:

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

Documentation:

User Guide

Directly from KeYmaera website : http://symbolaris.com/info/KeYmaera-guide.html

Documentation

Directly from KeYmaera website : http://symbolaris.com/info/KeYmaera.html#download

Related Publications

Directly from KeYmaera website : http://symbolaris.com/info/KeYmaera.html#publications

Developers:

André Platzer, Carnegie Mellon University, Pittsburgh, PA, USA

Jan-David Quesel, University of Oldenburg, Germany

Philipp Rümmer, Uppsala University, Sweden