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
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
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.