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: