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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Ahrendt, W., Beckert, B., Hähnle, R., Rümmer, P., & Schmitt, P. H. (2007). Verifying object-oriented programs with KeY: A tutorial. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4709 LNCS, pp. 70–101). Springer Verlag. https://doi.org/10.1007/978-3-540-74792-5_4
Mendeley helps you to discover research relevant for your work.