All posts by Richard Bubel

KeY: Deductive Verification of Software

This is a follow-up post to the blog about the verification of TimSort. Many people have asked how KeY actually works and which resources are available. In this brief post we answer some of the questions about KeY that came up in the discussions. We also provide pointers to documentation, case studies and technical papers.

The KeY project was started in the late 1990s at University of Karlsruhe (now: Karlsruhe Institute of Technology) with the aim to develop a tool for formal specification and verification of Java that would be useful not only to the formal methods specialist, but for ordinary software developers as well. This was an ambitious and long-term goal. After more than 15 years of research and tool development, it has been partially reached, as we explain below. For example, KeY not only includes a formal verification tool, but also a debugger with novel features and an automated test case generator. In the meantime, KeY is developed and maintained at three sites. In addition to Karlsruhe, these are Technische Universität Darmstadt and Chalmers University of Technology.

The core of KeY is a software verification tool based on symbolic execution and invariant reasoning. Continue reading