TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 15451

Verification of Evolving Graph Structures

( Nov 01 – Nov 06, 2015 )

(Click in the middle of the image to enlarge)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/15451

Organizers

Contact



Schedule

Motivation

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.

Summary

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.

This challenge has prompted several successful lines of research, developing novel techniques such as shape analysis, separation logic, forest automata, and several graph transformation-based approaches. 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 brought together researchers interested in developing precise and scalable techniques for the analysis of graph manipulations, i.e., techniques that are able to handle the challenges that arise in current verification problems. These challenges require novel developments and the 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 was to enhance common understanding and cross-fertilization, highlighting connections among the approaches via tutorials and working groups, with the explicit purpose to enhance interaction. Discussion topics included:

  • 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.

We invited four representatives of the different communities to give tutorial talks in order to introduce fundamental concepts and techniques. Specifically, the following four tutorial talks took place on the first day of the seminar:

  • Tomas Vojnar: Shape Analysis via Symbolic Memory Graphs and Its Application for Conversion of Pointer Programs to Container Programs
  • Giorgio Delzanno: Graphs in Infinite-State Model-Checking
  • Arend Rensink: Verification Techniques for Graph Rewriting
  • Viktor Vafeiadis: Separation Logic

On Tuesday and Thursday we organized the following working groups in order to discuss more specific topics which were of interest to a substantial part of the participants:

  • Benchmarks and Application Domains
  • Specification Languages for Graphs
  • Ownership
  • Graph Rewriting for Verification

The organizers would like to thank all the participants and speakers for their inspiring talks and many interesting discussions. Furthermore we would like to acknowledge Christina Jansen and Eugenio Orlandelli who helped to write and prepare this report. A special thanks goes to the Dagstuhl staff who were a great help in organizing this seminar.

Copyright Parosh Aziz Abdulla, Fabio Gadducci, Barbara König, and Viktor Vafeiadis

Participants
  • Mohamed-Faouzi Atig (Uppsala University, SE) [dblp]
  • Parosh Aziz Abdulla (Uppsala University, SE) [dblp]
  • Peter Backes (Universität des Saarlandes, DE) [dblp]
  • Paolo Baldan (University of Padova, IT) [dblp]
  • Ahmed Bouajjani (University of Paris VII, FR) [dblp]
  • Andrea Corradini (University of Pisa, IT) [dblp]
  • Aiswarya Cyriac (Uppsala University, SE) [dblp]
  • Giorgio Delzanno (University of Genova, IT) [dblp]
  • Cezara Dragoi (IST Austria - Klosterneuburg, AT) [dblp]
  • Constantin Enea (University of Paris VII, FR) [dblp]
  • Javier Esparza (TU München, DE) [dblp]
  • Fabio Gadducci (University of Pisa, IT) [dblp]
  • Silvio Ghilardi (University of Milan, IT) [dblp]
  • Holger Giese (Hasso-Plattner-Institut - Potsdam, DE) [dblp]
  • Christoph Haase (ENS - Cachan, FR) [dblp]
  • Annegret Habel (Universität Oldenburg, DE) [dblp]
  • Reiko Heckel (University of Leicester, GB) [dblp]
  • Alexander Heußner (Universität Bamberg, DE) [dblp]
  • Lukas Holik (Brno University of Technology, CZ) [dblp]
  • David Janin (University of Bordeaux, FR) [dblp]
  • Christina Jansen (RWTH Aachen, DE) [dblp]
  • Bengt Jonsson (Uppsala University, SE) [dblp]
  • Joost-Pieter Katoen (RWTH Aachen, DE) [dblp]
  • Barbara König (Universität Duisburg-Essen, DE) [dblp]
  • Tomer Kotek (TU Wien, AT) [dblp]
  • Narayan Kumar Krishnan (Chennai Mathematical Institute, IN) [dblp]
  • Leen Lambers (Hasso-Plattner-Institut - Potsdam, DE) [dblp]
  • Michele Loreti (University of Firenze, IT) [dblp]
  • Roland Meyer (TU Kaiserslautern, DE) [dblp]
  • Thomas Noll (RWTH Aachen, DE) [dblp]
  • Fernando Orejas (UPC - Barcelona, ES) [dblp]
  • Eugenio Orlandelli (CIS, IT) [dblp]
  • Oded Padon (Tel Aviv University, IL) [dblp]
  • Detlef Plump (University of York, GB) [dblp]
  • Chris Poskitt (ETH Zürich, CH) [dblp]
  • Arend Rensink (University of Twente, NL) [dblp]
  • Ahmed Rezine (Linköping University, SE) [dblp]
  • Leila Ribeiro (Federal University of Rio Grande do Sul, BR) [dblp]
  • Xavier Rival (ENS - Paris, FR) [dblp]
  • Arnaud Sangnier (University of Paris VII, FR) [dblp]
  • Richard Trefler (University of Waterloo, CA) [dblp]
  • Viktor Vafeiadis (MPI-SWS - Kaiserslautern, DE) [dblp]
  • Tomas Vojnar (Brno University of Technology, CZ) [dblp]
  • Thomas Wies (New York University, US) [dblp]
  • Florian Zuleger (TU Wien, AT) [dblp]

Classification
  • semantics / formal methods
  • verification / logic

Keywords
  • Verification
  • static analysis
  • graphs
  • graph transformation
  • heap analysis
  • shape analysis
  • separation logic
  • dynamic systems