Modern software systems must meet increasingly higher safety, security, and reliability standards. At the same time a new dimension of complexity is introduced by dynamic features: At program level, modern code relies on dynamic creation of objects and dynamic dispatch of methods. At system level, communication protocols, computer networks, and ubiquitous computing systems exhibit complex features involving process migration, remote execution or dynamic reconfiguration.

The aim of the project "Static Analysis of Dynamically Evolving Systems" is to develop verification and analysis methods for such dynamically evolving systems. Our approach focusses on a foundational specification technique for distributed and mobile systems, so-called graph transformation systems. In this framework dynamic features are modelled in a natural way by means of transformation rules over graphs, which represent system states.

Our automatic analysis techniques are based on established general methods such as abstract interpretation, type systems and model checking. In order to come to terms with the inherent difficulties in the analysis of graph transformation systems, we are also using more specific concepts such as graph morphisms and specialized techniques, e.g., unfoldings and approximation by Petri nets.

Finally our research includes the adaptation of different logical frameworks and specification languages to express properties of graph transformation systems and in order to use them as input for our verification tools.