Tutorial at IFM 2007

Integrating Object-oriented Design and
Deductive Verification of Software

Oxford, UK, July 3rd, 2007

Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt, Vladimir Klebanov

Materials

The slides of the tutorial are available as a printable PDF. Further materials, such as the KeY system itself, publications and details of the KeY book are available from the resp. sections of this website.

Outline

Formal methods can only gain widespread use in industrial software development if they are integrated:

into software development techniques, tools, and languages used in practice
with each other.

We use the KeY system 1.0 (developed by the tutorial presenters) to demonstrate our approach. KeY is an integrated deductive verification environment that allows full-functional verification of programs written in the full-featured object-oriented language Java Card. The deductive core of the system is a novel interactive/automated theorem prover for the Dynamic Logic for Java. The prover has an easy-to-use graphical interface and seamlessly integrates automated and interactive proving. On the software development side, the system integrates with industrial platforms Borland Together and Eclipse.

The tutorial will cover the following topics:

How to design and formally specify object-oriented software (different fomalisms: UML/OCL, JML; tool support)
Deductive analysis of designs and specifications in the KeY prover (e.g., checking structural subtyping)
Deductive verification of non-trivial Java implementations with the KeY prover
Integration of verification and testing - why and how; generating JUnit tests from proofs

Schedule

This is a half-day tutorial. It is held on Tuesday morning, July 3rd, 2007. Participation is included in the IFM conference fee.

08.30 - 09:00	Registration
09.00 - 10:45	Tutorial Part 1
10.45 - 11:15	Coffee Break
11.15 - 12:45	Tutorial Part 2
12.45 - 13:45	Lunch
13.45 -	IFM Technical Programme