This project is aimed at providing verification techniques for concurrent and distributed systems, modelled by graph transformation. For this we will use techniques from the areas of formal languages (especially recognizable graph languages) and graph theory (especially graph minor theory), between which close ties are known to exist.

We will further develop methods based on recognizable graph languages due to Courcelle and apply them to invariant checking, termination analysis and regular model checking. In this context we will also use monadic second-order logic for specifying graph languages.

In the second part of the project we will employ graph-theoretical results in order to obtain backwards analysis techniques for graph transformation systems. This is a new and original direction of research since so far little graph theory has been used for the verification of graph transformation.

In addition we will implement our techniques (or continue working on existing prototype tools) and apply them to various case studies.