KeY Variants

While KeY is mainly aimed at verification of Java / JavaCard programs, recent research has produced a number of KeY variants to handle related problems.

KeYmaera - A Deductive Verification Tool for Hybrid Systems

Run KeYmaera via Web Start[?]

It is a theorem prover extension implementing the calculus for the differential dynamic logic dL. KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies.

KeYmaera extends the KeY tool with real arithmetic, continuous dynamics and corresponding algorithms and proof strategies such that it can be used for practical verification of hybrid systems. It has been developed in the group of Prof. Ernst-Rüdiger Olderog at the University of Oldenburg and of André Platzer at Carnegie Mellon University.

  • KeYmaera: Download, information, examples and tutorials ..

KeY-Hoare - An Interactive Verification Tool for the Hoare Calculus

Run KeY-Hoare
via Web Start[?]

The standard KeY Tool uses Dynamic Logic as underlying logic. The Hoare Calculus is another possibility to deal with programs in logic. KeY-Hoare is built on top of KeY and features a Hoare calculus with updates. It is used in the Chalmers undergraduate course on Program Verification to teach the Hoare calculus.

More information and Download

KeY Flavours

KeY Concurrent

The KeY tool has been adapted to a fragment of multi-threaded Java. For more information about this project, please contact Vladimir Klebanov.

KeY for C

The KeY tool has been adapted to a subset of the C programming language. For more information about this project, please contact Reiner Hähnle.