KeY Tutorial

KeY Project Links: Tutorial Home Outline KeY Project Home

Tutorial at IFM 2007

Integrating Object-oriented Design and
Deductive Verification of Software

Oxford, UK, July 3rd, 2007

Bernhard Beckert, Reiner Hahnle, Peter H. Schmitt, Vladimir Klebanov

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

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: