 | 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)
|
 | |
 Screenshot of KeY 1.4 | |
| Developer(s) | Karlsruhe Institute of Technology, Technische Universität Darmstadt, Chalmers University of Technology |
|---|---|
| Stable release | 2.12.3
/ September 8, 2024[1] |
| Written in | Java |
| Operating system | Linux, Mac, Windows, Solaris |
| Available in | English |
| Type | Formal verification |
| License | GPL, version 2 |
| Website | www |
KeY is a formal verification tool for Java programs.[2] 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[3] or hybrid systems.[4] 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.
- ^ "Release KeY-2.12.3 (2024-09-08) · KeYproject/key". github.com. Retrieved 2025-04-26.
- ^ Ahrendt, Wolfgang; Beckert, Bernhard; Bubel, Richard; Hähnle, Reiner; Schmitt, Peter H.; Ulbrich, Mattias, eds. (2016). "Deductive Software Verification – The KeY Book". Lecture Notes in Computer Science. doi:10.1007/978-3-319-49812-6. ISSN 0302-9743.
- ^ Mürk, Oleg; Larsson, Daniel; Hähnle, Reiner (2007). Pfenning, Frank (ed.). "KeY-C: A Tool for Verification of C Programs". Automated Deduction – CADE-21. Berlin, Heidelberg: Springer: 385–390. doi:10.1007/978-3-540-73595-3_27. ISBN 978-3-540-73595-3.
- ^ Platzer, André; Quesel, Jan-David (2008). Armando, Alessandro; Baumgartner, Peter; Dowek, Gilles (eds.). "KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)". Automated Reasoning. Berlin, Heidelberg: Springer: 171–178. doi:10.1007/978-3-540-71070-7_15. ISBN 978-3-540-71070-7.
© MMXXIII Rich X Search. We shall prevail. All rights reserved. Rich X Search