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
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 08171

Beyond the Finite: New Challenges in Verification and Semistructured Data

( Apr 20 – Apr 25, 2008 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:

  • Anca Muscholl (University of Bordeaux, FR)
  • Ramaswamy Ramanujam (Chennai Mathematical Institute, IN)
  • Michaël Rusinowitch (INRIA Lorraine - Nancy, FR)
  • Thomas Schwentick (TU Dortmund, DE)
  • Victor Vianu (University of California - San Diego, US)



The seminar ran as scheduled, from the morning of April 21 until mid-day on April 25. Since the seminar was centred on 7 themes (as outlined in the proposal, the event was structured accordingly: 7 invited talks (ranging from 60 to 90 minutes each) on each of the themes, and 25 presentations from participants (of 30 minutes each). An excursion to Trier on Wednesday afternoon provided a cultural interlude in a dense academic programme. With extensive interaction and discussions, the seminar was lively (with some heated debates) and highly educative. The central objective of the seminar was to look for common questions and techniques between research on verification and data, and to learn from each other; this was achieved satisfactorily.

Certain techniques emerged as being centrally useful. For instance, the use of well-quasi orderings on configurations of infinite space systems to prove termination of verification algorithms surfaced many times in discussions, whether it be in the context of parameterized systems, or in systems communicating by messages, or in software verification. Similarly, reachability studies on counter systems of various kinds was seen to have implications for a variety of contexts: analysis of data, reasoning about timed systems, and real arithmetic. The use of symbolic techniques and powerful theorems on term rewriting systems was illustrated in the study of security protocols as well as that of tree automata. Questions on logical characterizations and the need for logics over infinite alphabets was emphasized time and again, not only in the context of databases, but also in discussions on verification of parameterized systems and metric temporal logics. The need for decidable relational logics that combine quantification and order was talked of in the context of web services.

While logic and automata theory provided the lingua franca for the seminar, the discussions were not exclusively on these. There were presentations, especially in the context of software verification, on modelling issues as well as the use of (theorem proving and model checking) tools, and the pragmatics necessary in such a context.

The Dagstuhl setting, with its unique atmosphere of a castle set in an idyllic scene, backed by excellent organization and amenities, provided just the right tone for the seminar, allowing participants to focus on research interaction. With a mix of experienced and young researchers taking active part, we can confidently expect that the seminar will lead to new collaborations and applications of infinite-state systems benefiting both the verification and database areas.

  • Serge Abiteboul (INRIA SaclaY, FR) [dblp]
  • Parosh Aziz Abdulla (Uppsala University, SE) [dblp]
  • Henrik Björklund (TU Dortmund, DE) [dblp]
  • Bernard Boigelot (University of Liège, BE) [dblp]
  • Mikolaj Bojanczyk (University of Warsaw, PL) [dblp]
  • Ahmed Bouajjani (University of Paris VII, FR) [dblp]
  • Patricia Bouyer-Decitre (ENS - Cachan / CNRS - LSV, FR) [dblp]
  • Supratik Chakraborty (Indian Institute of Technology - Mumbai, IN) [dblp]
  • Jorge R. Cuéllar (Siemens AG - München, DE) [dblp]
  • Deepak D'Souza (Chennai Mathematical Institute, IN) [dblp]
  • Claire David (University of Paris VII, FR) [dblp]
  • Stéphanie Delaune (ENS - Cachan, FR) [dblp]
  • Stéphane Demri (ENS - Cachan, FR)
  • Alin Deutsch (University of California - San Diego, US) [dblp]
  • Javier Esparza (TU München, DE) [dblp]
  • Gaelle Fontaine (University of Amsterdam, NL) [dblp]
  • Wouter Gelade (Hasselt University - Diepenbeek, BE)
  • Blaise Genest (IRISA / CNRS, FR) [dblp]
  • Florent Jacquemard (ENS - Cachan, FR) [dblp]
  • Michael Kaminski (Technion - Haifa, IL)
  • Bakh Khoussainov (University of Auckland, NZ) [dblp]
  • Felix Klaedtke (ETH Zürich, CH) [dblp]
  • Pavel Krcal (Uppsala University, SE)
  • Ranko Lazic (University of Warwick - Coventry, GB) [dblp]
  • Christof Löding (RWTH Aachen, DE) [dblp]
  • Wim Martens (TU Dortmund, DE) [dblp]
  • Maarten Marx (University of Amsterdam, NL)
  • Antoine Miné (ENS - Paris, FR) [dblp]
  • Madhavan Mukund (Chennai Mathematical Institute, IN)
  • Markus Müller-Olm (Universität Münster, DE) [dblp]
  • Anca Muscholl (University of Bordeaux, FR) [dblp]
  • Martin Otto (TU Darmstadt, DE) [dblp]
  • Shaz Qadeer (Microsoft Research - Redmond, US) [dblp]
  • Ramaswamy Ramanujam (Chennai Mathematical Institute, IN) [dblp]
  • Michaël Rusinowitch (INRIA Lorraine - Nancy, FR)
  • Philippe Schnoebelen (ENS - Cachan, FR) [dblp]
  • Nicole Schweikardt (Universität Frankfurt, DE) [dblp]
  • Thomas Schwentick (TU Dortmund, DE) [dblp]
  • Luc Segoufin (ENS - Cachan, FR) [dblp]
  • Helmut Seidl (TU München, DE) [dblp]
  • Olivier Serre (University Paris-Diderot, FR)
  • Axel Simon (ENS - Paris, FR) [dblp]
  • S.P. Suresh (Chennai Mathematical Institute, IN)
  • Wolfgang Thomas (RWTH Aachen, DE) [dblp]
  • Jan Van den Bussche (Hasselt University - Diepenbeek, BE) [dblp]
  • Kumar Neeraj Verma (TU München, DE)
  • Victor Vianu (University of California - San Diego, US) [dblp]
  • Igor Walukiewicz (University of Bordeaux, FR) [dblp]
  • Volker Weber (TU Dortmund, DE)
  • Marc Zeitoun (University of Bordeaux, FR) [dblp]

  • data bases / information retrieval
  • data structures / algorithms / complexity
  • security / cryptography
  • semantics / specification / formal methods
  • verification / logic

  • verification
  • semistructured data
  • infinite state systems
  • logic
  • automata