Tutorial at CADE-20

Integrating Object-oriented Design and
Deductive Verification of Software

Tallinn, Estonia, Saturday July 23, 2005
14:00-18:00

Wolfgang Ahrendt, Reiner Hähnle, Vladimir Klebanov, Philipp Rümmer

Outline

Deductive methods can only gain widespread use in industrial software development if they are integrated into software development techniques, tools, and languages that are used in practice.

The objective of this tutorial is to show how formal specification and deductive verification of object-oriented programs can be done within a software development platform that supports contemporary design and implementation methodologies. The KeY Tool (co-developed by the tutorial presenters), which implements this approach, will be used for demonstration purposes.

The tutorial covers:

1. Design and specification of object-oriented programs.
2. Deductive analysis of design and formal specification.
3. Deductive verification of implementations.
4. Selected issues in the verification of object-oriented programs.

Although we concentrate in this tutorial on particular languages (UML/OCL, Java), the presented ideas, problems, and solutions apply to other object-oriented design and implementation languages as well.

Materials

Slides

Here are the slides as a PDF slide show and in printer-friendly version with 4 slides per page.

Survey paper

Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, Peter H. Schmitt
The KeY Tool. Software and Systems Modeling, volume 4, number 1, Springer, 2005
Abstract - Bibtex

Demo .key files

The .key input files for most of the demos are here. They can be used with the stand-alone version of the KeY prover by simply loading them.

KeY Prover

The KeY version that was used for the demos and the libraries necessary to run this version. Instructions on how to install and to run KeY can be found here.

Bank Example

The eclipse project containing the bank-software example that was used in some of the demos. The system is annotated with JML constraints and can also be loaded and verified using the KeY standalone prover.

Links

The KeY Project

Presenters

Wolfgang Ahrendt is a senior lecturer in Computer Science at Chalmers University of Technology in Göteborg (Sweden). His main interests are automated theorem proving and disproving, as well as software verification and specification.

Reiner Hähnle is professor of Computer Science at Chalmers University of Technology in Göteborg (Sweden). His main interests are integrated deductive software verification, software specification, automated theorem proving, and multi valued logic.

Vladimir Klebanov is a PhD student in Computer Science at the University of Koblenz-Landau (Germany). His main interests are integrated deductive software verification, proof reuse in program verification, and the verification of parallel systems.

Philipp Rümmer is a PhD student in Computer Science at Chalmers University of Technology in Göteborg (Sweden). His main interests are integrated deductive software verification, disproving of software correctness, and the verification of parallel systems.