On model checking the dynamics of object-based software : a foundational approach
Dino Distefano · University of Twente Research Information · 2003
This dissertation is concerned with software verication, in particular automated techniques to assess the correct functioning of object-based programs. We focus on the dynamic aspects of these programs and consider model-checking based verication techniques. The major obstacle to the design of modelchecking algorithms is the innite state-space explosion caused by the dynamic constructs supported by object-based languages.