Formal specification and verification techniques can improve the quality of object-oriented software by enabling semantic checks and certification of properties. To be applicable to object-oriented programs, they have to cope with subtyping, aliasing via object references, as well as abstract and recursive methods. For mastering the resulting complexity, mechanical aid is needed. The article outlines the specific technical requirements for the specification and verification of object-oriented programs. Based on these requirements, it argues that verification of OO-programs should be done interactively and develops an modular architecture for this task. In particular, it shows how to integrate interactive program verification with existing universal interactive theorem provers, and explains the new developed parts of the architecture. To underline the general approach, we describe interesting features of our prototype implementation.

integration of verification systems, program verification, object-oriented programming