Verifying Object-Oriented Programs with KeY: A Tutorial
Wolfgang Ahrendt, Bernhard Beckert, Reiner H\"ahnle,
Philipp R\"ummer, and Peter H. Schmitt
This paper is a tutorial on performing formal specification and
semi-automatic verification of Java programs with the formal
software development tool KeY. This tutorial aims to fill the gap
between elementary introductions using toy examples and state-of-art
case studies by going through a self-contained, yet non-trivial,
example. It is hoped that this contributes to explain the problems
encountered in verification of imperative, object-oriented programs
to a readership outside the limited community of active researchers.