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:
The material for my course is on this page.