Reiner Hähnle,
Chalmers University of Technology and Gothenburg University

Formal Analysis of Java Programs with KeY

Abstract

The KeY system is a formal software analysis tool for the Java programming language based on symbolic execution of Java source code. It can be used not only to formally verify Java programs against specification contracts written in JML (Java Modeling Language), but also to generate test cases with high code coverage and to debug programs by visualizing symbolic execution trees. We give a brief introduction into the underlying theoretical concepts of KeY (dynamic logic, symbolic execution, contracts, invariants) followed by hands-on exercises with practical analysis tasks.

We assume basic familiarity with first-order logic, operational semantics, and object-oriented programming. The KeY system is freely available from the project website and runs on Unix/Linux, Mac, Windows that have Java installed.

---

Information from the lecturer: To prepare for my course:

• Please refresh your knowledge on first-order logic and on Java, if necessary; we will essentially use typed first-order logic to specify contracts of programs. The logic and a decuction system is described in depth in Chapter 2 of Verification of Object-Oriented Software: The KeY Approach.
• As a very leightweight introduction to the KeY system you can read Chapter 1 of this book.
• Please make sure that you can download, install and run KeY 1.4 TP3 from this page.

The material for my course is on this page.