Beyond the Finite: New Challenges in Verification and Semistructured Data

Summary

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.