Dagstuhl Seminar Proceedings, Volume 8332

Document

08332 Abstracts Collection – Distributed Verification and Grid Computing

Authors: Henri E. Bal, Lubos Brim, and Martin Leucker

Abstract

From 08/10/2008 to 08/14/2008 the Dagstuhl Seminar 08332 ``Distributed Verification and Grid Computing'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Henri E. Bal, Lubos Brim, and Martin Leucker. 08332 Abstracts Collection – Distributed Verification and Grid Computing. In Distributed Verification and Grid Computing. Dagstuhl Seminar Proceedings, Volume 8332, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{bal_et_al:DagSemProc.08332.1,
  author =	{Bal, Henri E. and Brim, Lubos and Leucker, Martin},
  title =	{{08332 Abstracts Collection – Distributed Verification and Grid Computing}},
  booktitle =	{Distributed Verification and Grid Computing},
  pages =	{1--10},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8332},
  editor =	{Henri E. Bal and Lubos Brim and Martin Leucker},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08332.1},
  URN =		{urn:nbn:de:0030-drops-16335},
  doi =		{10.4230/DagSemProc.08332.1},
  annote =	{Keywords: Parallel Model Checking, Grid Computing, Verification}
}

Document

DOI: 10.4230/DagSemProc.08332.2

08332 Executive Summary – Distributed Verification and Grid Computing

Authors: Henri E. Bal, Lubos Brim, and Martin Leucker

Abstract

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.

Cite as

Henri E. Bal, Lubos Brim, and Martin Leucker. 08332 Executive Summary – Distributed Verification and Grid Computing. In Distributed Verification and Grid Computing. Dagstuhl Seminar Proceedings, Volume 8332, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{bal_et_al:DagSemProc.08332.2,
  author =	{Bal, Henri E. and Brim, Lubos and Leucker, Martin},
  title =	{{08332 Executive Summary – Distributed Verification and Grid Computing}},
  booktitle =	{Distributed Verification and Grid Computing},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8332},
  editor =	{Henri E. Bal and Lubos Brim and Martin Leucker},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08332.2},
  URN =		{urn:nbn:de:0030-drops-16329},
  doi =		{10.4230/DagSemProc.08332.2},
  annote =	{Keywords: Grid computing, verification, parallel computing, model checking}
}

Document

DOI: 10.4230/DagSemProc.08332.3

A Typical Verification Challenge for the GRID

Authors: Jaco van de Pol

Abstract

A typical verification challenge for the GRID community is presented. The concrete challenge is to implement a simple recursive algorithm for finding the strongly connected components in a graph. The graph is typically stored in the collective memory of a number of computers, so a distributed algorithm is necessary. The implementation should be efficient and scalable, and separate synchronization and implementation details from the purely algorithmic aspects. In the end, a framework is envisaged for distributed algorithms on very large graphs. This would be useful to explore various alternative algorithmic choices.

Cite as

Jaco van de Pol. A Typical Verification Challenge for the GRID. In Distributed Verification and Grid Computing. Dagstuhl Seminar Proceedings, Volume 8332, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{vandepol:DagSemProc.08332.3,
  author =	{van de Pol, Jaco},
  title =	{{A Typical Verification Challenge for the GRID}},
  booktitle =	{Distributed Verification and Grid Computing},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8332},
  editor =	{Henri E. Bal and Lubos Brim and Martin Leucker},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08332.3},
  URN =		{urn:nbn:de:0030-drops-16293},
  doi =		{10.4230/DagSemProc.08332.3},
  annote =	{Keywords: Strongly connected components, distributed algorithms, breadth first search}
}

Document

DOI: 10.4230/DagSemProc.08332.4

Efficient Large-Scale Model Checking

Authors: Kees Verstoep, Henri E. Bal, Jiri Barnat, and Lubos Brim

Abstract

Model checking is a popular technique to systematically and automatically verify system properties. Unfortunately, the well-known state explosion problem often limits the extent to which it can be applied to realistic specifications, due to the huge resulting memory requirements. Distributed memory model checkers exist, but have thus far only been evaluated on small-scale clusters, with mixed results. We examine one well-known distributed model checker in detail, and show how a number of additional optimizations in its runtime system enable it to efficiently check very demanding problem instances on a large-scale, multi-core compute cluster. We analyze the impact of the distributed algorithms employed, the problem instance characteristics and network overhead. Finally, we show that the model checker can even obtain good performance in a high-bandwidth computational grid environment.

Cite as

Kees Verstoep, Henri E. Bal, Jiri Barnat, and Lubos Brim. Efficient Large-Scale Model Checking. In Distributed Verification and Grid Computing. Dagstuhl Seminar Proceedings, Volume 8332, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{verstoep_et_al:DagSemProc.08332.4,
  author =	{Verstoep, Kees and Bal, Henri E. and Barnat, Jiri and Brim, Lubos},
  title =	{{Efficient Large-Scale Model Checking}},
  booktitle =	{Distributed Verification and Grid Computing},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8332},
  editor =	{Henri E. Bal and Lubos Brim and Martin Leucker},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08332.4},
  URN =		{urn:nbn:de:0030-drops-16309},
  doi =		{10.4230/DagSemProc.08332.4},
  annote =	{Keywords: Distributed model checking, Grid-based model checking}
}

Document

DOI: 10.4230/DagSemProc.08332.5

Verification of MPI-based Computations

Authors: Stephen F. Siegel

Abstract

The Message Passing Interface is a widely-used parallel programming model and is the effective standard for high-performance scientific computing. It has also been used in parallel model checkers, such as DiVinE. In this talk we discuss the verification problem for MPI-based programs. The MPI is quite large and the semantics complex. Nevertheless, by restricting to a certain subset of MPI, the verification problem becomes tractable. Certain constructs outside of this subset (such as wildcard receives) can lead to a rapid blowup in the number of states, but MPI-specific reduction techniques have led to progress in combating this state explosion. Specifying correctness is another challenge. One approach is to use a trusted sequential version of the program as the specification, and use model checking and symbolic execution techniques to establish the functional equivalence of the sequential and parallel versions. This approach is supported in extsc{Mpi-Spin}, an extension to the model checker extsc{Spin} for verifying MPI-based programs.

Cite as

Stephen F. Siegel. Verification of MPI-based Computations. In Distributed Verification and Grid Computing. Dagstuhl Seminar Proceedings, Volume 8332, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{siegel:DagSemProc.08332.5,
  author =	{Siegel, Stephen F.},
  title =	{{Verification of MPI-based Computations}},
  booktitle =	{Distributed Verification and Grid Computing},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8332},
  editor =	{Henri E. Bal and Lubos Brim and Martin Leucker},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08332.5},
  URN =		{urn:nbn:de:0030-drops-16316},
  doi =		{10.4230/DagSemProc.08332.5},
  annote =	{Keywords: MPI, Spin, model checking, MPI-Spin, symbolic execution}
}

Dagstuhl Seminar Proceedings, Volume 8332

Publication Details

Access Numbers

Documents

08332 Abstracts Collection – Distributed Verification and Grid Computing

Abstract

Cite as

08332 Executive Summary – Distributed Verification and Grid Computing

Abstract

Cite as

A Typical Verification Challenge for the GRID

Abstract

Cite as

Efficient Large-Scale Model Checking

Abstract

Cite as

Verification of MPI-based Computations

Abstract

Cite as

Filters

Thanks for your feedback!

Could not send message