Graph-based software specification and verification

The (in)correct functioning of many software systems heavily influences how we qualify our daily lives. Software companies as well as academic computer science research groups spend much effort on applying and developing techniques for improving the correctness of software systems. In this dissertation we focus on using and developing graph-based techniques to specify and verify the behaviour of software systems in general, and object-oriented systems more specically. We elaborate on two ways to improve the correctness (and thereby the quality) of such systems.
Firstly, we investigate the potential of using the graph transformation technique to formally specify the dynamic semantics of (object-oriented) programming languages. Those semantics are typically specied in natural language. Such specications are often hard to understand or even ambiguous. We show how the graph transformation framework provides formal and intuitive means for their specication.
Secondly, we develop techniques to verify systems of which the behaviour is specied as graph production systems. For the verication of such systems, we introduce an algorithm that combines a well-known on-the-y model checking algorithm with ideas from bounded model checking. One of the main problems of model checking is the state-explosion problem. This problem is often tackled using partial order reduction techniques. Unfortunately, many such techniques are based on assumptions that do not hold for graph production systems. Therefore, we develop a new dynamic partial order reduction algorithm based on selecting so-called probe sets and prove its correctness.
Most of the techniques developed in this dissertation have been implemented in the graph transformation tool GROOVE.