KeY

This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these messages) This article includes a list of general references, but it lacks sufficient corresponding inline citations. Please help to improve this article by introducing more precise citations. (August 2016) (Learn how and when to remove this message) This article may be too technical for most readers to understand. Please help improve it to make it understandable to non-experts, without removing the technical details. (March 2019) (Learn how and when to remove this message) (Learn how and when to remove this message)

KeY

Screenshot of KeY 1.4
Developer(s)	Karlsruhe Institute of Technology, Technische Universität Darmstadt, Chalmers University of Technology
Stable release	2.10.0 / December 23, 2021 (2021-12-23)[1]
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.