Arnd Poetzsch-Heffter,
Universität Kaiserslautern

Modular verification of object-oriented programs

Abstract

Modular verification techniques support the specification of program parts and allow to prove that the parts satisfy their specification in all admissible program contexts in which the parts can be used. Modularity is an important prerequisite for scalability of verification techniques. Object-oriented programming comes with two difficulties for modularity: reference aliasing and subtyping with dynamic method binding. In combination with data abstraction and specifications ranging over several classes, modular verification in object-oriented programming becomes a challenging problem.

In this course, we consider modular verification of functional, invariant, and frame properties in object-oriented programming. The course introduces the underlying challenges and discusses shortcomings of the classical visible state approach. The central part of the course presents different modular verification frameworks based on ownership techniques.

Information from the lecturer: To prepare for my course:

• Please refresh your knowledge as suggested for Hähnle's course.
• As a very lightweight introduction to Spec# look at the talk "Program Verification Using the Spec# Programming System" available from this page.
• If possible, install Spec#. For instructions, see this page.

Lecture slides: lecture 1, lecture 2.

Lab session material.