Program Verification – The KeY Project

Contents

Supported Java Features
Tutorials
Relevant blog posts
Literature

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, a tool to statically remove Generics from the code can be downloaded here.
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

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

23 entries « ‹ 1 of 3 › »

2018

Steinhöfel, Dominic; Hähnle, Reiner

Modular, Correct Compilation with Automatic Soundness Proofs Inproceedings

In: Margaria, Tiziana; Steffen, Bernhard (Ed.): Leveraging Applications of Formal Methods, Verification and Validation. Modeling, pp. 424–447, Springer International Publishing, Cham, 2018, ISSN: 0302-9743.

Abstract | Links | BibTeX

2017

de Gouw, Stijn; de Boer, Frank S; Bubel, Richard; Hähnle, Reiner; Rot, Jurriaan; Steinhöfel, Dominic

Verifying OpenJDK's Sort Method for Generic Collections Journal Article

In: Journal of Automated Reasoning, 2017, ISSN: 1573-0670.

Abstract | Links | BibTeX

Steinhöfel, Dominic; Wasser, Nathan

A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows Inproceedings

In: Polikarpova, Nadia; Schneider, Steve (Ed.): Integrated Formal Methods - 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings, pp. 279–294, Springer, 2017.

Links | BibTeX

2016

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

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

In: 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

In: 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

@phdthesis{ TUD-CS-2016-0099,

title = {Integrating Symbolic Execution, Debugging and Verification},

author = {Martin Hentschel},

year = {2016},

date = {2016-01-01},

school = {Technische Universit\"{a}t Darmstadt},

abstract = {In modern software development, almost all activities are centered around an integrated development environment (IDE). Besides the main use cases to write, execute and debug source code, an IDE serves also as front-end for other tools involved in the development process such as a version control system or an application lifecycle management. Independent from the applied development process, the techniques to ensure correct software are always the same. The general goal is to find defects as soon as possible, because the sooner a defect is found, the easier and cheaper it is to fix. In the first place, the programming language helps to prevent some kinds of defects. Once something is written, it is effective to review it not only to find defects, but also to increase its quality. Also tools which statically analyze the source code help to find defects automatically. In addition, testing is used to ensure that selected usage scenarios behave as expected. However, a test can only show the presence of a failure and not its absence. To ensure that a program is correct, it needs to be proven that the program complies to a formal specification describing the desired behavior. This is done by formal verification tools. Finally, whenever a failure is observed, debugging takes place to locate the defect. This thesis extends the software development tool suite by an interactive debugger based on symbolic execution, a technique to explore all feasible execution paths up to a given depth simultaneously. Such a tool can not only be used for classical debugging activities, but also during code reviews or in order to present results of an analysis based on symbolic execution. The contribution is an extension of symbolic execution to explore the full program behavior even in presence of loops and recursive method calls. This is achieved by integrating specifications in form of loop invariants and methods contracts into a symbolic execution engine. How such a symbolic execution engine based on verification proofs can be realized is presented as well. In addition, the presented Symbolic Execution Debugger (SED) makes the Eclipse platform ready for debuggers based on symbolic execution. Its functionality goes beyond that of traditional interactive debuggers. For instance, debugging can start directly at any method or statement and all program execution paths are explored simultaneously. To support program comprehension, program execution paths as well as intermediate states are visualized. By default, the SED comes with a symbolic execution engine implemented on top of the KeY verification system. Statistical evidence that the SED increases effectiveness of code reviews is gained from a controlled experiment. Another novelty of the SED is that arbitrary verification proofs can be inspected. Whereas traditional user interfaces of verification tools present proof states in a mathematical fashion, the SED analyzes the full proof and presents different aspects of it using specialized views. A controlled experiment gives statistical evidence that proof understanding tasks are more effective using the SED by comparing its user interface with the original one of KeY. The SED allows one to interact with the underlying prover by adapting code and specifications in an auto-active flavor, which creates the need to manage proofs directly within an IDE. A presented concept achieves this, by integrating a semi-automatic verification tool into an IDE. It includes several optimizations to reduce the overall proof time and can be realized without changing the verification tool. An optimal user experience is achieved only if all aspects of verification are directly supported within the IDE. Thus a thorough integration of KeY into Eclipse is presented, which for instance includes in addition to the proof management capabilities to edit JML specifications and to setup the needed infrastructure for verification with KeY. Altogether, a platform for tools based on symbolic execution and related to verification is presented, which offers a seamless integration into an IDE and furthers a usage in combination. Furthermore, many aspects, like the way the SED presents proof attempts to users, help to reduce the barrier of using formal methods.},

keywords = {},

pubstate = {published},

tppubtype = {phdthesis}

}

In modern software development, almost all activities are centered around an integrated development environment (IDE). Besides the main use cases to write, execute and debug source code, an IDE serves also as front-end for other tools involved in the development process such as a version control system or an application lifecycle management. Independent from the applied development process, the techniques to ensure correct software are always the same. The general goal is to find defects as soon as possible, because the sooner a defect is found, the easier and cheaper it is to fix. In the first place, the programming language helps to prevent some kinds of defects. Once something is written, it is effective to review it not only to find defects, but also to increase its quality. Also tools which statically analyze the source code help to find defects automatically. In addition, testing is used to ensure that selected usage scenarios behave as expected. However, a test can only show the presence of a failure and not its absence. To ensure that a program is correct, it needs to be proven that the program complies to a formal specification describing the desired behavior. This is done by formal verification tools. Finally, whenever a failure is observed, debugging takes place to locate the defect. This thesis extends the software development tool suite by an interactive debugger based on symbolic execution, a technique to explore all feasible execution paths up to a given depth simultaneously. Such a tool can not only be used for classical debugging activities, but also during code reviews or in order to present results of an analysis based on symbolic execution. The contribution is an extension of symbolic execution to explore the full program behavior even in presence of loops and recursive method calls. This is achieved by integrating specifications in form of loop invariants and methods contracts into a symbolic execution engine. How such a symbolic execution engine based on verification proofs can be realized is presented as well. In addition, the presented Symbolic Execution Debugger (SED) makes the Eclipse platform ready for debuggers based on symbolic execution. Its functionality goes beyond that of traditional interactive debuggers. For instance, debugging can start directly at any method or statement and all program execution paths are explored simultaneously. To support program comprehension, program execution paths as well as intermediate states are visualized. By default, the SED comes with a symbolic execution engine implemented on top of the KeY verification system. Statistical evidence that the SED increases effectiveness of code reviews is gained from a controlled experiment. Another novelty of the SED is that arbitrary verification proofs can be inspected. Whereas traditional user interfaces of verification tools present proof states in a mathematical fashion, the SED analyzes the full proof and presents different aspects of it using specialized views. A controlled experiment gives statistical evidence that proof understanding tasks are more effective using the SED by comparing its user interface with the original one of KeY. The SED allows one to interact with the underlying prover by adapting code and specifications in an auto-active flavor, which creates the need to manage proofs directly within an IDE. A presented concept achieves this, by integrating a semi-automatic verification tool into an IDE. It includes several optimizations to reduce the overall proof time and can be realized without changing the verification tool. An optimal user experience is achieved only if all aspects of verification are directly supported within the IDE. Thus a thorough integration of KeY into Eclipse is presented, which for instance includes in addition to the proof management capabilities to edit JML specifications and to setup the needed infrastructure for verification with KeY. Altogether, a platform for tools based on symbolic execution and related to verification is presented, which offers a seamless integration into an IDE and furthers a usage in combination. Furthermore, many aspects, like the way the SED presents proof attempts to users, help to reduce the barrier of using formal methods.

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

A General Lattice Model for Merging Symbolic Execution Branches Inproceedings

In: 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

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

Links | BibTeX

Wasser, Nathan

Automatic generation of specifications using verification tools = Automatische Spezifikationserzeugung mit Hilfe von Verifikationswerkzeugen PhD Thesis

Darmstadt University of Technology, Germany, 2016.

Links | BibTeX

2015

Mostowski, Wojciech; Ulbrich, Mattias

Dynamic Dispatch for Method Contracts through Abstract Predicates Inproceedings

In: 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

23 entries « ‹ 1 of 3 › »