Abstract:

We intend to verify object-oriented software through model checking,
by representing program states as graphs and execution steps as
derivations from graph production rules. We propose the resulting
state space model as an alternative to traditional, state vector-
based models. In this talk I will discuss the pros and cons of this
approach, touching upon diverse aspects such as algorithmic
complexity, symmetries, partial order reduction, representation
techniques, logics for expressing properties, and abstraction.
The approach has been partially implemented in a state space 
generation tool "GROOVE" (Graphs for Object-Oriented Verification), 
which I will also demonstrate.