CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Verifying Object-Oriented Programs with KeY: A Tutorial

Wolfgang Ahrendt (Institutionen för data- och informationsteknik (Chalmers)) ; Bernhard Beckert ; Reiner Hähnle (Institutionen för data- och informationsteknik (Chalmers)) ; Philipp Rümmer ; Peter H. Schmitt
Formal Methods for Components and Objects, eds. de Boer, Bonsangue, Graf, de Roever Vol. LNCS 4709 (2007),
[Konferensbidrag, refereegranskat]

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.

Nyckelord: software verification, Java, JML, formal specification

Denna post skapades 2007-12-21. Senast ändrad 2008-12-11.
CPL Pubid: 63857


Institutioner (Chalmers)

Institutionen för data- och informationsteknik (Chalmers)
Institutionen för data- och informationsteknik, datavetenskap (GU) (GU)



Chalmers infrastruktur