Key

KeY

Screenshot of KeY 1.4
Developer(s)	Karlsruhe Institute of Technology, Technische Universität Darmstadt, Chalmers University of Technology
Stable release	2.4.1 / February 19, 2015 (2015-02-19)
Preview release	2.5.1178 / October 6, 2015 (2015-10-06)
Development status	Active
Written in	Java
Operating system	Linux, Mac, Windows, Solaris
Available in	English
Type	Formal verification
License	GPL
Website	www.key-project.org

The KeY tool is used in formal verification of Java programs. It accepts specifications written in the Java Modeling Language to Java source files. These are transformed into theorems of dynamic logic and then compared against program semantics that are likewise defined in terms of dynamic logic. KeY is significantly powerful in that it supports both interactive (i.e. by hand) and fully automated correctness proofs. Failed proof attempts can be used for a more efficient debugging or verification-based testing. There have been several extensions to KeY in order to apply it to the verification of C programs or hybrid systems. KeY is jointly developed by Karlsruhe Institute of Technology, Germany; Technische Universität Darmstadt, Germany; and Chalmers University of Technology in Gothenburg, Sweden and is licensed under the GPL.

The usual user input to KeY consists of a Java source file with annotations in JML. Both are translated to KeY's internal representation, dynamic logic. From the given specifications, several proof obligations arise which are to be discharged, i.e. a proof has to be found. To this ends, the program is symbolically executed with the resulting changes to program variables stored in so-called updates. Once the program has been processed completely, there remains a first-order logic proof obligation. At the heart of the KeY system lies a first-order theorem prover based on sequent calculus, which is used to close the proof. Interference rules are captured in so called taclets which consist of an own simple language to describe changes to a sequent.