10. – 14. August 2008, Dagstuhl-Seminar 08332

Distributed Verification and Grid Computing


Henri E. Bal (VU University Amsterdam, NL)
Lubos Brim (Masaryk University – Brno, CZ)
Martin Leucker (TU München, DE)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Seminar Proceedings DROPS


The Dagstuhl Seminar on "Distributed Verification and Grid Computing" took place from 10.08.2008 to 14.08.2008 and brought together two groups of researchers to discuss their recent work and recent trends related to parallel verification of large scale computer systems on large scale grids. In total, 29 experts from 12 countries attended the seminar.

The computing power of computers has increased by a factor of a million over the past couple of decades. As a matter of fact, the development effort, both in industry and in academia, has gone into developing bigger, more powerful and more complex applications. In the next few decades we may still expect a similar rate of growth, due to various factors such as continuing miniaturization, parallel, and distributed computing.

With the increase in complexity of computer systems, it becomes even more important to develop formal methods for ensuring their quality and reliability. Various techniques for automated and semi-automated analysis and verification have been successfully applied to real-life computer systems. However, these techniques are computationally demanding and memory-intensive in general and their applicability to extremely large and complex systems routinely seen in practice these days is limited. The major hampering factor is the state space explosion problem due to which large industrial models cannot be efficiently handled unless we use more sophisticated and scalable methods and a balance of the usual trade-off between run-time, memory requirements, and precision of a method.

Recently, an increasing interest in parallelizing and distributing verification techniques has emerged, especially in the light of new multi-core architectures. On the other hand, grid computing is an emerging technology that enables large-scale resource sharing and coordinated problem solving within distributed systems. By providing scalable, secure, high-performance mechanisms for discovering and negotiating access to remote resources, Grid technologies promise to make it possible for scientific collaborations to share resources on an unprecedented scale that was previously impossible.

As such, grid computing promises to be an ideal partner to tackle huge verification tasks. However, while the verification community started to work out cluster based verification solutions, there is limited knowledge about grids. Similarly, while the grid community developed general grid infrastructure, highly optimized domain specific solutions first developed for the verification community might emerge to general solutions improving the state-of-the-art in grid computing.

The 17 talks given during this seminar were split into two main streams: distributed verification related topics and grid computing related presentations. Two overview talks aimed at brief introductions to respective domains. The presentations were complemented by a huge number of informal discussions, in which, for example, a typical verification challenge for the GRID has been identified and addressed. Moreover, the scientific work was enriched also by several non-scientific activities like several table tennis matches and a traditional hike. The friendly atmosphere stimulated collaborations among the different communities that have already resulted in joint papers.


  • Semantics / Specification / Formal Methods
  • Verification / Logic Own Categories: Parallel Computing
  • Grid Computing


  • Grid computing
  • Verification
  • Parallel computing
  • Model checking


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

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.


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