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.
Verificationproceeds 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.
KeYhas 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
http://www.key-project.org/download/releases/key26-pre/webstart/KeY.jnlpIn December 2016, "
Deductive Software Verification - The KeY Book" appeared as Springer LNCS volume 10001 - the definitive guide to
KeY.