Program Verification

This page is under construction

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.
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, the eclipse extension comes along with a plugin to statically remove Generics from the code.
Floating point types Unsupported.
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

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

KeY: The Sequent Calculus of the KeY Tool

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.

Verifying Object-Oriented Programs with KeY: A Tutorial

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.

Literature

18 entries « 1 of 2 »

2016

Hentschel, Martin; Hähnle, Reiner; Bubel, Richard

An Empirical Evaluation of Two User Interfaces of an Interactive Program Verifier Inproceedings

Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, pp. 403-413, ACM, Singapore, Singapore, 2016, ISBN: 978-1-4503-3845-5.

Abstract | BibTeX

Hentschel, Martin; Hähnle, Reiner; Bubel, Richard

The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts Inproceedings

Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, pp. 846–851, ACM, Singapore, Singapore, 2016, ISBN: 978-1-4503-3845-5.

Abstract | BibTeX

Hentschel, Martin

Integrating Symbolic Execution, Debugging and Verification PhD Thesis

Technische Universität Darmstadt, 2016.

Abstract | BibTeX

Scheurer, Dominic; Hähnle, Reiner; Bubel, Richard

A General Lattice Model for Merging Symbolic Execution Branches Inproceedings

Ogata, Kazuhiro; Lawford, Mark; Liu, Shaoying (Ed.): Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 14-18, 2016, Proceedings, pp. 57–73, Springer International Publishing, 2016.

Abstract | Links | BibTeX

Mostowski, Wojciech; Ulbrich, Mattias

Dynamic Dispatch for Method Contracts Through Abstract Predicates Journal Article

Trans. Modularity and Composition, 1 , pp. 238–267, 2016.

Links | BibTeX

2015

Mostowski, Wojciech; Ulbrich, Mattias

Dynamic Dispatch for Method Contracts through Abstract Predicates Inproceedings

Proceedings of the 14th International Conference on Modularity, MODULARITY 2015, Fort Collins, CO, USA, March 16 - 19, 2015, pp. 109–116, ACM, 2015.

Links | BibTeX

Bruns, Daniel; Mostowski, Wojciech; Ulbrich, Mattias

Implementation-level Verification of Algorithms with KeY Journal Article

Software Tools for Technology Transfer, 17 (6), pp. 729–744, 2015, ISSN: 1433-2779.

Abstract | Links | BibTeX

Küsters, Ralf; Truderung, Tomasz; Beckert, Bernhard; Bruns, Daniel; Kirsten, Michael; Mohr, Martin

A Hybrid Approach for Proving Noninterference of Java Programs Inproceedings

Fournet, Cédric; Hicks, Michael (Ed.): 28th IEEE Computer Security Foundations Symposium (CSF 2015), pp. 305-319, 2015.

Abstract | Links | BibTeX

Küsters, Ralf; Truderung, Tomasz; Beckert, Bernhard; Bruns, Daniel; Kirsten, Michael; Mohr, Martin

A Hybrid Approach for Proving Noninterference of Java Programs Journal Article

IACR Cryptology ePrint Archive, 2015 , pp. 438, 2015.

Abstract | Links | BibTeX

2014

Ghazi, Aboubakr Achraf El; Ulbrich, Mattias; Gladisch, Christoph; Tyszberowicz, Shmuel; Taghdiri, Mana

JKelloy: A Proof Assistant for Relational Specifications of Java Programs Inproceedings

NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29 - May 1, 2014. Proceedings, pp. 173–187, 2014.

Links | BibTeX

18 entries « 1 of 2 »