Volume

Dagstuhl Seminar Proceedings, Volume 6081

Publication Details

  • published at: 2006-11-09
  • Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Access Numbers

Documents

No documents found matching your filter selection.
Document
DOI: 10.4230/DagSemProc.06081.1
06081 Abstracts Collection – Software Verification: Infinite-State Model Checking and Static Program Analysis

Authors: Parosh Aziz Abdulla, Ahmed Bouajjani, and Markus Müller-Olm

Abstract
From 19.02.06 to 24.02.06, the Dagstuhl Seminar 06081 ``Software Verification: Infinite-State Model Checking and Static Program Analysis'' 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 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

Parosh Aziz Abdulla, Ahmed Bouajjani, and Markus Müller-Olm. 06081 Abstracts Collection – Software Verification: Infinite-State Model Checking and Static Program Analysis. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:DagSemProc.06081.1,
  author =	{Abdulla, Parosh Aziz and Bouajjani, Ahmed and M\"{u}ller-Olm, Markus},
  title =	{{06081 Abstracts Collection – Software Verification: Infinite-State Model Checking and Static Program Analysis}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06081.1},
  URN =		{urn:nbn:de:0030-drops-7997},
  doi =		{10.4230/DagSemProc.06081.1},
  annote =	{Keywords: Software verification, infinite-state systems, static program analysis, automatic analysis}
}
Document
DOI: 10.4230/DagSemProc.06081.2
06081 Executive Summary – Software Verification: Infinite-State Model Checking and Static Program Analysis

Authors: Parosh Aziz Abdulla, Ahmed Bouajjani, and Markus Müller-Olm

Abstract
{\em Software systems} are present at the very heart of many daily-life applications, such as in communication (telephony and mobile Internet), transportation, energy, health, etc. Such systems are very often {\em critical}\/ in the sense that their failure can have considerable human/economical consequences. In order to ensure reliability, development methods must include {\em algorithmic analysis and verification techniques} which allow (1) to detect automatically defective behaviors of the system and to analyze their source, and (2) to check that every component of a system conforms to its specification. Two important and quite active research communities are particularly concerned with this challenge: the community of computer-aided verification, especially the community of (infinite-state) model checking, and the community of static program analysis. From 19.02.06 to 24.02.06, 51 researchers from these two communities met at the Dagstuhl Seminar 06081 ``Software Verification: Infinite-State Model Checking and Static Program Analysis'' in order to improve and deepen the mutual understanding of the developed technologies and to trigger collaborations. During the seminar which was held at the International Conference and Research Center (IBFI), Schloss Dagstuhl, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar are put together in this paper.
Cite as

Parosh Aziz Abdulla, Ahmed Bouajjani, and Markus Müller-Olm. 06081 Executive Summary – Software Verification: Infinite-State Model Checking and Static Program Analysis. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:DagSemProc.06081.2,
  author =	{Abdulla, Parosh Aziz and Bouajjani, Ahmed and M\"{u}ller-Olm, Markus},
  title =	{{06081 Executive Summary – Software Verification: Infinite-State Model Checking and Static Program Analysis}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--5},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06081.2},
  URN =		{urn:nbn:de:0030-drops-7973},
  doi =		{10.4230/DagSemProc.06081.2},
  annote =	{Keywords: Infinite-state systems, model checking, program analysis, software verification}
}
Document
DOI: 10.4230/DagSemProc.06081.3
Analysis of Dynamic Communicating Systems by Hierarchical Abstraction

Authors: Jörg Bauer and Reinhard Wilhelm

Abstract
We propose a new abstraction technique for verifying topology properties of dynamic communicating systems (DCS), a special class of infinite-state systems. DCS are characterized by unbounded creation and destruction of objects along with an evolving communication connectivity or topology. We employ a lightweight graph transformation system to specify DCS. Hierarchical Abstraction (HA) computes a bounded over-approximation of all topologies that can occur in a DCS directly from its transformation rules. HA works in two steps. First, for each connected component, called cluster, of a topology, objects sharing a common property are summarized to one abstract object. Then isomorphic abstract connected components are summarized to one abstract component, called abstract cluster. This yields a conservative approximation of all graphs that may occur during any DCS run. The technique is implemented.
Cite as

Jörg Bauer and Reinhard Wilhelm. Analysis of Dynamic Communicating Systems by Hierarchical Abstraction. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{bauer_et_al:DagSemProc.06081.3,
  author =	{Bauer, J\"{o}rg and Wilhelm, Reinhard},
  title =	{{Analysis of Dynamic Communicating Systems by Hierarchical Abstraction}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--25},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06081.3},
  URN =		{urn:nbn:de:0030-drops-7271},
  doi =		{10.4230/DagSemProc.06081.3},
  annote =	{Keywords: Graph transformation, Abstract Interpretation, Shape Analysis}
}
Document
DOI: 10.4230/DagSemProc.06081.4
Flat counter automata almost everywhere!

Authors: Jérôme Leroux and Grégoire Sutre

Abstract
This paper argues that flatness appears as a central notion in the verification of counter automata. A counter automaton is called flat when its control graph can be ``replaced'', equivalently w.r.t. reachability, by another one with no nested loops. From a practical view point, we show that flatness is a necessary and sufficient condition for termination of accelerated symbolic model checking, a generic semi-algorithmic technique implemented in successful tools like FAST, LASH or TReX. From a theoretical view point, we prove that many known semilinear subclasses of counter automata are flat: reversal bounded counter machines, lossy vector addition systems with states, reversible Petri nets, persistent and conflict-free Petri nets, etc. Hence, for these subclasses, the semilinear reachability set can be computed using a emph{uniform} accelerated symbolic procedure (whereas previous algorithms were specifically designed for each subclass).
Cite as

Jérôme Leroux and Grégoire Sutre. Flat counter automata almost everywhere!. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{leroux_et_al:DagSemProc.06081.4,
  author =	{Leroux, J\'{e}r\^{o}me and Sutre, Gr\'{e}goire},
  title =	{{Flat counter automata almost everywhere!}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--19},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06081.4},
  URN =		{urn:nbn:de:0030-drops-7297},
  doi =		{10.4230/DagSemProc.06081.4},
  annote =	{Keywords: Symbolic representation, Infinite state system, Acceleration, Meta-transition}
}
Document
DOI: 10.4230/DagSemProc.06081.5
Lazy Shape Analysis

Authors: Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz

Abstract
Many software model checkers are based on predicate abstraction. If the verification goal depends on pointer structures, the approach does not work well, because it is difficult to find adequate predicate abstractions for the heap. In contrast, shape analysis, which uses graph-based heap abstractions, can provide a compact representation of recursive data structures. We integrate shape analysis into the software model checker BLAST. Because shape analysis is expensive, we do not apply it globally. Instead, we ensure that, like predicates, shape graphs are computed and stored locally, only where necessary for proving the verification goal. To achieve this, we extend lazy abstraction refinement, which so far has been used only for predicate abstractions, to three-valued logical structures. This approach does not only increase the precision of model checking, but it also increases the efficiency of shape analysis. We implemented the technique by extending BLAST with calls to TVLA.
Cite as

Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz. Lazy Shape Analysis. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{beyer_et_al:DagSemProc.06081.5,
  author =	{Beyer, Dirk and Henzinger, Thomas A. and Th\'{e}oduloz, Gr\'{e}gory},
  title =	{{Lazy Shape Analysis}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--16},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06081.5},
  URN =		{urn:nbn:de:0030-drops-7284},
  doi =		{10.4230/DagSemProc.06081.5},
  annote =	{Keywords: Software model checking, Shape analysis, Counterexample-guided abstraction refinement, Interpolation, Predicate abstraction}
}
Document
DOI: 10.4230/DagSemProc.06081.6
Reachability analysis of multithreaded software with asynchronous communication

Authors: Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, and Jan Strejcek

Abstract
We introduce asynchronous dynamic pushdown networks (ADPN), a new model for multithreaded programs in which pushdown systems communicate via shared memory. ADPN generalizes both CPS (concurrent pushdown systems) and DPN (dynamic pushdown networks). We show that ADPN exhibit several advantages as a program model. Since the reachability problem for ADPN is undecidable even in the case without dynamic creation of processes, we address the bounded reachability problem, which considers only those computation sequences where the (index of the) thread accessing the shared memory is changed at most a fixed given number of times. We provide efficient algorithms for both forward and backward reachability analysis. The algorithms are based on automata techniques for symbolic representation of sets of configurations. This talk is based on joint work with Ahmed Bouajjani, Javier Esparza, and Jan Strejcek that appeared in FSTTCS 2005.
Cite as

Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, and Jan Strejcek. Reachability analysis of multithreaded software with asynchronous communication. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{bouajjani_et_al:DagSemProc.06081.6,
  author =	{Bouajjani, Ahmed and Esparza, Javier and Schwoon, Stefan and Strejcek, Jan},
  title =	{{Reachability analysis of multithreaded software with asynchronous communication}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06081.6},
  URN =		{urn:nbn:de:0030-drops-7263},
  doi =		{10.4230/DagSemProc.06081.6},
  annote =	{Keywords: Model checking, pushdown systems, concurrency}
}

Filters

  • Authors
  • A
  • Abdulla, Parosh Aziz
  • B
  • Bauer, Jörg
  • Beyer, Dirk
  • Bouajjani, Ahmed
  • E
  • Esparza, Javier
  • H
  • Henzinger, Thomas A.
  • L
  • Leroux, Jérôme
  • M
  • Müller-Olm, Markus
  • S
  • Schwoon, Stefan
  • Strejcek, Jan
  • Sutre, Grégoire
  • T
  • Théoduloz, Grégory
  • W
  • Wilhelm, Reinhard

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact