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 template messages)
|
Developer(s) | Karlsruhe Institute of Technology, Technische Universität Darmstadt, Chalmers University of Technology |
---|---|
Stable release | 2.10.0
/ December 23, 2021[1] |
Written in | Java |
Operating system | Linux, Mac, Windows, Solaris |
Available in | English |
Type | Formal verification |
License | GPL |
Website | www |
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.
Overview
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
Java Card DL
The theoretical foundation of KeY is a
Deduction component
At the heart of the KeY system lies a first-order theorem prover based on a sequent calculus. A sequent is of the form where (assumptions) and (propositions) are sets of formulas with the intuitive meaning that holds true. By means of deduction, an initial sequent representing the proof obligation is shown to be constructible from just fundamental first-order axioms (such as equality ).
Symbolic execution of Java code
During that, program modalities are eliminated by symbolic execution. For instance, the formula is logically equivalent to . As this example shows, symbolic execution in dynamic logic is very similar to calculating
Example
Suppose one wants to prove that the following method calculates the product of some non-negative integers and .
int foo (int x, int y) {
int z = 0;
while (y > 0)
if (y % 2 == 0) {
x = x*2;
y = y/2;
} else {
y = y/2;
z = z+x;
x = x*2;
}
return z;
}
One thus starts the proof with the premise and the to-be-shown conclusion . Note that tableaux of sequent calculi are usually written "upside-down", i.e., the starting sequent appears at the bottom and deduction steps go upwards. The proof can be seen in the figure on the right.
Additional features
Symbolic Execution Debugger
The Symbolic Execution Debugger visualizes the control flow of a program as a symbolic execution tree that contains all feasible execution paths through the program up to a certain point. It is provided as a plugin to the Eclipse development platform.
Test Case Generator
KeY is usable as a
Distribution and Variants of the KeY System
KeY is free software written in Java and licensed under
KeY-Hoare
KeY-Hoare is built on top of KeY and features a
KeYmaera/KeYmaeraX
KeYmaera [1] (previously called HyKeY) is a deductive verification tool for hybrid systems based on a calculus for the differential dynamic logic dL [2]. It extends the KeY tool with computer algebra systems like
KeYmaera has been developed at the University of Oldenburg and the Carnegie Mellon University. The name of the tool was chosen as a homophone to Chimera, the hybrid animal from ancient Greek mythology.
KeYmaeraX [3] developed at the Carnegie Mellon University is the successor of KeYmaera. It has been completely rewritten.
KeY for C
KeY for C is an adaption of the KeY System to
ASMKeY
There is also an adaptation to use KeY for the symbolic execution of
References
- ^ "Download – The KeY Project". key-project.org. Retrieved 2021-04-13.
Sources
- Verification of Object-Oriented Software: The KeY Approach. Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (Eds.). ISBN 978-3-540-68977-5.
- Deductive Software Verification – The KeY Book: From Theory to Practice. Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, Mattias Ulbrich (Eds.). ISBN 978-3-319-49812-6
- A comparison of tools for teaching formal software verification. Ingo Feinerer and Gernot Salzer. Springer, 2008
- Programming With Proofs: Language Based Approaches To Totally Correct Software. Aaron Stump. Verified Software: Theories, Tools, and Experiments, 2005.
- High Assurance (for Security or Safety) and Free-Libre / Open Source Software (FLOSS). David Wheeler, 2009