As of March 15, 2011, this page is no longer maintained. KeYHeap has become the regular development version of KeY (version 1.7), and is scheduled to replace the stable release version KeY 1.6 in the future. For up-to-date information see the KeY download page.

"KeYHeap" is the working title of a major revision of the KeY system that is currently under development. At its core, KeYHeap is a deductive verifier for sequential Java programs wrt. specifications written in a crossover between JML and dynamic frames. Unlike all KeY versions <= 1.6, KeYHeap uses a heap model like that of typical Boogie-based verifiers (in particular VeriCool and Dafny, which also use dynamic frames style specifications).


Presentation Slides

Download the Latest KeY Development Version

Java web start:Run KeY now

[Internal wiki page]


Some features of KeY 1.6 currently unsupported in KeYHeap


Benjamin Weiß