KeY

Screenshot of the KeY tool. The correctness of a charge routine on an electronic cash smart card has been shown automatically.

The KeY tool is used in formal verification of Java programs. It accepts both specifications written in JML or OCL. These are transformed into theorems of dynamic logic and then compared against program semantics which 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. It can be integrated into CASE tools to extract specifications. 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 the University of Karlsruhe, Chalmers University of Technology in Gothenburg, and the University of Koblenz and is licensed under the GPL.

Java Card DL

The theoretical foundation of KeY is a formal logic called Java Card DL. It is a version of 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 φ. Proofs of the validity of such formulas can then be performed by means of a sequent calculus and symbolic execution.

Other Supported Logics

Besides the core tool based on Java Card DL, there are several variants of KeY which support reasoning for other kinds of logics:

• Differential dynamic logic (dL) [1] (KeYmaera [2], external) (*)
• Logic for Abstract state machines [3] (ASMKeY, external)
• Dynamic Logic for MISRA C [4] (KeY-C)
• A logic for JCSP programs [5]

(*) under active development/maintained

Variants of the KeY System

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.

The Symbolic Execution Debugger is provided as a plugin to the Eclipse development platform.

KeY-Hoare

KeY-Hoare is built on top of KeY and features a Hoare calculus with state updates. State updates are a means of describing state transitions in a Kripke structure.

KeYmaera

KeYmaera [6] (previously called HyKeY) is a deductive verification tool for hybrid systems based on a calculus for the differential dynamic logic dL [7]. It extends the KeY tool with computer algebra systems like Mathematica and corresponding algorithms and proof strategies such that it can be used for practical verification of hybrid systems.

KeYmaera has been developed at the University of Oldenburg and the Carnegie Mellon University.

KeY Test Case Generator

KeY is usable as a model-based testing tool that can generate unit tests for Java programs. The model from which test data and the test case are derived consists of a formal specification (provided in JML or OCL) and a symbolic execution tree of the implementation under test which is computed by the KeY system.

KeY for C

KeY for C is an adaption of the KeY System to MISRA C, a subset of the C programming language.

Sources

• Verification of Object-Oriented Software: The KeY Approach. Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (Eds.). Springer, 2007. ISBN 978-3-540-68977-5.
• 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.

See also

• Abstract state machines
• B-Method
• BLAST
• ESC/Java2
• KIV
• Spec#

External links

• Home page of the KeY project
• FOL/bussproofs patch Small ad-hoc patch (for v.1.4.0) to export nicely formatted FOL proof trees to using the bussproofs package.