Dagstuhl Seminar 08332
Distributed Verification and Grid Computing
( Aug 10 – Aug 14, 2008 )
Permalink
Organizers
- Henri E. Bal (VU University Amsterdam, NL)
- Lubos Brim (Masaryk University - Brno, CZ)
- Martin Leucker (TU München, DE)
Contact
- Annette Beyer (for administrative matters)
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.
- Henri E. Bal (VU University Amsterdam, NL) [dblp]
- Jiri Barnat (Masaryk University - Brno, CZ)
- Jörg Behrend (Universität Tübingen, DE)
- Stefan Blom (University of Twente, NL)
- Lubos Brim (Masaryk University - Brno, CZ)
- Ivana Cerná (Masaryk University - Brno, CZ) [dblp]
- Gianfranco Ciardo (University of California - Riverside, US)
- Wan Fokkink (VU University Amsterdam, NL)
- Ganesh L. Gopalakrishnan (University of Utah - Salt Lake City, US) [dblp]
- Sergei Gorlatch (Universität Münster, DE)
- Jan Friso Groote (Eindhoven Univ. of Technology, NL) [dblp]
- Keijo Heljanko (Helsinki University of Technology, FI)
- Fabrice Huet (INRIA Sophia Antipolis - Méditerranée, FR)
- Joost-Pieter Katoen (RWTH Aachen, DE) [dblp]
- Thilo Kielmann (VU University Amsterdam, NL) [dblp]
- Josva Kleist (Nordic DataGrid Facility, DK)
- Krzysztof Kurowski (Polish Supercomputing Center - Poznan, PL)
- Martin Leucker (TU München, DE) [dblp]
- Gerald Lüttgen (Universität Bamberg, DE) [dblp]
- Pradeep Nalla (Universität Tübingen, DE)
- Simona Orzan (TU Eindhoven, NL)
- Andrey Rybalchenko (MPI-SWS - Saarbrücken, DE) [dblp]
- Fernando Schapachnik (University of Buenos Aires, AR)
- Stephen Siegel (University of Delaware, US)
- Kenjiro Taura (University of Tokyo, JP) [dblp]
- Jaco van de Pol (University of Twente, NL) [dblp]
- Michael Weber (University of Twente, NL)
- Verena Wolf (Universität des Saarlandes, DE) [dblp]
- Ramin Yahyapour (TU Dortmund, DE) [dblp]
Classification
- semantics / specification / formal methods
- verification / logic Own Categories: parallel computing
- grid computing
Keywords
- grid computing
- verification
- parallel computing
- model checking