The KeY Formal Verification Tool

Date/Time: Thursday 4 May 2017, 6.00pm - 9.00pm

BCS, 1st Floor, The Davidson Building, 5 Southampton Street, London, WC2E 7HA | Maps

Prof Dr. Reiner Hähnle, TU Darmstadt, Germany



KeY is a deductive verification tool for sequential Java programs. It is based on a rich program logic for Java source code. KeY can perform functional verification of Java programs annotated with with specifications in the Java Modeling language. Specification elements include class invariants and method contracts. The rules of KeY's program logic realize a symbolic execution engine for Java. Verification proceeds method-wise, unbounded loops are approximated by invariants, method calls by contracts. KeY incorporates state-of-art proof search and an auto-active mode that in many cases results in fully automatic proofs. Otherwise, the user can perform interactive steps or ask the system to search for a counter example. KeY has been successfully used to verify complex legacy code, such as the JDK's sort method, where a subtle bug was found and subsequently fixed. I will explain some of the theoretical underpinnings and design principles of KeY. I will also give a live demonstration of some of KeY's capabilities.

Further information:
The KeY system can be downloaded and installed from

In December 2016, "Deductive Software Verification - The KeY Book" appeared as Springer LNCS volume 10001 as the definitive guide to KeY.


PDF Icon The KeY Formal Verification Tool - Prof Dr. Reiner Hähnle