The SPIN extension presented in this article is meant as a way to facilitate the modeling and verification of object-oriented programs. It provides means for the formal representation of some run-time mechanisms intensively used in OO software, such as dynamic object creation and deletion, virtual function calls, etc. This article presents a number of language extensions along with their implementation in SPIN. We carried out a number of experiments and found out that an important expressibility gain can be achieved with at most a small loss of performance.