KeY

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 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. Java Card DL The theoretical foundation of KeY is a formal logic called Java Card DL. DL stands for Dynamic Logic. It is a version of a first-order dynamic logic tailored to Java Card programs. As such, it for example allows statements (formulas) like , which intuitively says that the post-condition must hold in all program states reachable by executing the Java Card program in any state that satisfies the pre-condition . This is equivalent to in Hoare calculus if and are purely first order. Dynamic logic, however, extends Hoare logic in that formulas may contain nested program modalities such as , or that quantification over formulas which contain modalities is possible. There is also a dual modality which includes termination.