Tutorial at SEFM 2006

Integrating Object-oriented Design and
Deductive Verification of Software

Pune, India, September 11-15, 2006

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

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.