Program Verification

The core feature of KeY is a theorem prover for Java Dynamic Logic based on a sequent calculus. It allows for full functional verification of sequential Java (without floats, garbage collection and multithreading, see the section below) and Java Card 2.2.x programs. Properties can be specified in the Java Modelling Language (JML) or in Java Dynamic Logic directly. To try out KeY for program verification, go to the download page and follow the instructions. Upon start of KeY, you can select among several examples in menu “File > Load Examples”. Read the corresponding descriptions and try out what looks most interesting to you. Alternatively, have a look at our tutorials section.

Supported Java Features

Java is a very complex language which massively evolved over the time. KeY does not support all Java features. Some of those, like floating-point arithmetic, are in principle hard to handle from a theorem-proving point of view; others, like Generics and Lambdas, could be considered in future versions of the system. The following (incomplete) table gives an overview about the state of selected Java features in the current KeY version. Features shaded in green are supported, those in red are unsupported; features in yellow are in principle not supported, but can be treated with restrictions by a workaround supplied by KeY. A list of supported JML features is available here.
Feature State
Basic Java 1.2 features KeY supports Integer arithmetic (for both mathematical Integers and actual Integer types with overflows), Strings, inheritance, dynamic dispatch, loops, recursion, …
Enhanced “for” loops Supported.
Floating point types Supported, reasoning via axioms and by using SMT solvers with float support.
Library methods KeY will throw an error when you use libraries the code of which is not in KeY’s classpath. However, we have a plugin in our eclipse extension which can create stubs with default contracts for library methods such that you can directly start proving properties about your code, or manually refine the stub specifications before.
Generics Unsupported; However, a tool to statically remove Generics from the code can be downloaded here.
Multithreading Unsupported.
try-with-resources and multi-catch (both Java 7) Unsupported.
Java 8 features (lambdas etc.) Unsupported.

Tutorials

Video Tutorial: Interactive Verification with the Symbolic Execution Debugger (SED)

Video Tutorial: Proof Attempt Inspection with the Symbolic Execution Debugger

Formal Verification with KeY: A Tutorial (2016)

By Bernhard Beckert, Reiner Hähnle, Martin Hentschel and Peter H. Schmitt Book chapter of the KeY book. This chapter gives a systematic tutorial introduction on how to perform formal program verification with the KeY system. It illustrates a number of complications and pitfalls, notably programs with loops, and shows how to deal with them. After working through this tutorial, you should be able to formally verify with KeY the correctness of simple Java programs, such as standard sorting algorithms, gcd, etc. Find this tutorial on SpringerLink

Note: The following tutorials may require older versions of KeY.

Verifying Object-Oriented Programs with KeY: A Tutorial (2007)

By Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Philipp Rümmer, and Peter H. Schmitt. Abstract. This paper is a tutorial on performing formal specification and semi-automatic verification of Java programs with the formal software development tool KeY. This tutorial aims to fill the gap between elementary introductions using toy examples and state-of-art case studies by going through a self-contained, yet non-trivial, example. It is hoped that this contributes to explain the problems encountered in verification of imperative, object-oriented programs to a readership outside the limited community of active researchers. Download this tutorial.

KeY: The Sequent Calculus of the KeY Tool (2015)

Tutorial at CADE-25 by Reiner Hähnle and Peter H. Schmitt You can download part I and part II of the slides of this tutorial as well as the corresponding KeY proofs.

Relevant blog posts

Norwegian Governmental Election Software Formally Verified with KeY - In his recently finished Master's thesis, Henrik Torland Klev verified (parts of) EVA, the main support system for elections in municipalities and counties in Norway, using the KeY prover.
Proving the Correctness of Program Transformations with Abstract Execution and REFINITY - Summary. Abstract Execution (AE) is a new program analysis technique for automatically proving second-order properties about programs. It is based on the symbolic execution of abstract programs with second-order symbolic stores.
Proving JDK’s Dual Pivot Quicksort Correct - by Bernhard Beckert, Jonas Schiffl, Peter H. Schmitt and Mattias Ulbrich Sorting is a fundamental functionality in libraries, for which efficiency is crucial. Correctness of the highly optimized implementations is often taken for granted. De Gouw et al. have shown that this certainty is deceptive by revealing a bug in the Java Development Kit (JDK) […]
New Feature: State Merging in KeY - Current nightly builds of KeY contain a new feature called state merging, a technique to decrease the size of proof trees arising from the symbolic execution of large programs.

Literature

26 entries « 3 of 3 »

2012

Beckert, Bernhard; Bruns, Daniel

Formal Semantics of Model Fields in Annotation-based Specifications Proceedings Article

In: Glimm, Birte; Krüger, Antonio (Ed.): KI 2012: Advances in Artificial Intelligence, pp. 13–24, Springer-Verlag, 2012, ISBN: 978-3-642-33346-0.

Abstract | Links | BibTeX

Beckert, Bernhard; Bruns, Daniel

Dynamic Trace Logic: Definition and Proofs Technical Report

Department of Informatics, Karlsruhe Institute of Technology no. 2012,10, 2012, ISSN: 2190-4782, (A revised version replacing an unsound rule is available at http://formal.iti.kit.edu/~bruns/papers/trace-tr.pdf).

Abstract | Links | BibTeX

2011

Ulbrich, Mattias; Geilmann, Ulrich; Ghazi, Aboubakr Achraf El; Taghdiri, Mana

On Proving Alloy Specifications using KeY Technical Report

Karlsruhe Institute of Technology no. 2011-37, 2011.

BibTeX

Schmitt, Peter H.; Ulbrich, Mattias; Weiß, Benjamin

Dynamic Frames in Java Dynamic Logic Proceedings Article

In: Beckert, Bernhard; Marché, Claude (Ed.): Revised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), pp. 138–152, Springer, 2011.

BibTeX

2005

Darvas, Ádám; Hähnle, Reiner; Sands, Dave

A Theorem Proving Approach to Analysis of Secure Information Flow Proceedings Article

In: Hutter, Dieter; Ullmann, Markus (Ed.): Proc. 2nd International Conference on Security in Pervasive Computing, pp. 193–209, Springer-Verlag, 2005.

Links | BibTeX

2003

Darvas, Ádám; Hähnle, Reiner; Sands, Dave

A Theorem Proving Approach to Analysis of Secure Information Flow Proceedings Article

In: Gorrieri, Roberto (Ed.): Workshop on Issues in the Theory of Security, WITS, IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS 2003.

BibTeX

26 entries « 3 of 3 »