. "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\u00E4t Darmstadt, Germany; and Chalmers University of Technology in Gothenburg, "@en . . . . . . . "2020-12-18"^^ . . . . . "Le logiciel KeY est un outil de v\u00E9rification formelle de programmes Java. D\u00E9but\u00E9 en 1998, le projet KeY est port\u00E9 par l'Institut de technologie de Karlsruhe, l'Universit\u00E9 de technologie de Darmstadt et l'\u00C9cole polytechnique Chalmers. KeY accepte les sp\u00E9cifications \u00E9crites \u00E0 l'aide du Java Modeling Language (JML)."@fr . "KeY"@en . . . . "Key-tool.jpg"@en . . . "2020-12-18"^^ . . . . . "KeY logo.svg"@en . . . . . "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\u00E4t Darmstadt, Germany; and Chalmers University of Technology in Gothenburg, Sweden and is licensed under the GPL."@en . . . . . . . . "KeY (logiciel)"@fr . . . "12528650"^^ . . . . . . . . . . . . . . . . . "English"@en . . . "2.8.0" . . . . . . . . . "KeY"@en . . . . . . . . . . . "Le logiciel KeY est un outil de v\u00E9rification formelle de programmes Java. D\u00E9but\u00E9 en 1998, le projet KeY est port\u00E9 par l'Institut de technologie de Karlsruhe, l'Universit\u00E9 de technologie de Darmstadt et l'\u00C9cole polytechnique Chalmers. KeY accepte les sp\u00E9cifications \u00E9crites \u00E0 l'aide du Java Modeling Language (JML)."@fr . . . . . "11416"^^ . "KeY"@en . . . . . . "2.8"^^ . . . . . . . . "Screenshot of KeY 1.4"@en . . . . . . . . "Linux, Mac, Windows, Solaris"@en . . . "1076362210"^^ . . . .