20. – 25. April 2008, Dagstuhl-Seminar 08171

Beyond the Finite: New Challenges in Verification and Semistructured Data


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)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Seminar Proceedings DROPS


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.


  • Data Bases / Information Retrieval
  • Data Structures / Algorithms / Complexity
  • Security / Cryptography
  • Semantics / Specification / Formal Methods
  • Verification / Logic


  • Verification
  • Semistructured data
  • Infinite state systems
  • Logic
  • Automata


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.