Locking Bugs Out with KeY
A Case Study on Automated Formal Verification of Java Programs
T. Kochar (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Benedikt Ahrens – Mentor (TU Delft - Programming Languages)
K.F. Wullaert – Mentor (TU Delft - Programming Languages)
M. Izadi – Graduation committee member (TU Delft - Software Engineering)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
KeY prover has been used to verify parts of the OpenJDK library and Norwegian election software, making it one of the most capable tools for formally verifying Java programs. However, an intuitive explanation of its theoretical foundations, capabilities and limitations is not available and the tool itself has a steep learning curve. This greatly increases the amount of effort to understand the tool sufficiently well to evaluate its suitability for ones needs. Here we implement two case studies to develop an intuition for the working of the tool in practice, exploring what properties can or cannot be expressed as specifications and what verifying correctness with KeY means. We find that the learning curve for KeY is even steeper than expected and conclude that it can be used to verify very complex functional and even some non-functional properties of sequential Java 7 code, conditioned on the capabilities of the user.