Tutorial at CADE-20

Integrating Object-oriented Design and
Deductive Verification of Software

Chapter

Selected issues in the verification of object-oriented programs

In this final part of the tutorial, we present particularly interesting aspects of (object-oriented) program verification that are topics of current research, which could be:

• Aliasing (different object variables can point to the same object).
• Integer arithmetic (a proper treatment of the gap between mathematical integers and Java integers).
• Modularisation of verification proofs.