01.11.15 - 06.11.15, Seminar 15451

Verification of Evolving Graph Structures

The following text appeared on our web pages prior to the seminar, and was included as part of the invitation.


Despite significant progress in recent years, verification still remains a challenging task for hardware and software systems. A particularly complex verification problem is the analysis of graph-like structures that may modify their topology during runtime. The main reason for the difficulty is that some features give rise to infinite state spaces. Examples include variables ranging over unbounded domains, timing constraints, dynamic process creation, heap manipulation, multi-threading, and dynamically allocated data structures. An additional source of complication is that the underlying graphs may be continuously evolving. There is no a priori bound on the size of the graphs that may arise when modelling the run of a program, and the graph shapes may change during a given execution.

The challenge prompted several successful lines of research, developing novel techniques such as shape analysis, separation logic, forest automata, and several graph transformation-based approaches, among others. Although specialized tools have been developed in each application area, a considerable amount of effort is needed to develop uniform frameworks that yield efficient yet general solutions.

This seminar brings together researchers interested in developing precise and scalable techniques for analysing graph manipulations, i.e., techniques that are able to handle the challenges that arise in current verification problems. These challenges require novel development and combination of techniques from a wide range of different areas including model checking and dynamic and static program analysis. By creating collaboration opportunities we hope to substantially increase the size of the systems that can be tackled and the precision of analysis that can be achieved.

Hence the main goal of this seminar is to enhance common understanding and cross-fertilization, highlighting connections among the approaches via survey talks and working groups, with the explicit purpose to enhance interaction. Discussion topics will include

  • the definition of uniform frameworks in which to integrate methods for graph analysis that have been proposed by the different research communities;
  • the development of new abstraction techniques for pushing the state-of-the-art of graph algorithms in program verification and model checking applications; and
  • the identification of research areas in which the analysis of graph manipulation may play an important role, such as the analysis of security protocols, social networks, adaptive networks, and biological systems.