Volume

Dagstuhl Seminar Proceedings, Volume 6172

Publication Details

  • published at: 2007-03-22
  • Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Access Numbers

Documents

No documents found matching your filter selection.
Document
DOI: 10.4230/DagSemProc.06172.1
06172 Abstracts Collection – Directed Model Checking

Authors: Stefan Edelkamp, Stefan Leue, and Willem Visser

Abstract
From 26.04.06 to 29.04.06, the Dagstuhl Seminar 06172 ``Directed Model Checking'' 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

Stefan Edelkamp, Stefan Leue, and Willem Visser. 06172 Abstracts Collection – Directed Model Checking. In Directed Model Checking. Dagstuhl Seminar Proceedings, Volume 6172, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{edelkamp_et_al:DagSemProc.06172.1,
  author =	{Edelkamp, Stefan and Leue, Stefan and Visser, Willem},
  title =	{{06172 Abstracts Collection – Directed Model Checking}},
  booktitle =	{Directed Model Checking},
  pages =	{1--11},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6172},
  editor =	{Stefan Edelkamp and Stefan Leue and Willem Visser},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06172.1},
  URN =		{urn:nbn:de:0030-drops-9469},
  doi =		{10.4230/DagSemProc.06172.1},
  annote =	{Keywords: Model Checking, Artificial Intelligence, AI Plannning, Guided Traversal, State Explosion Problem}
}
Document
DOI: 10.4230/DagSemProc.06172.2
06172 Executive Summary – Directed Model Checking

Authors: Stefan Edelkamp, Stefan Leue, and Willem Visser

Abstract
This is a summary of the Dagstuhl Seminar 06172 {em Directed Model Checking} that was held 26 - 29 April 2006 at Schloss Dagstuhl, Germany. Directed Model Checking is a software and hardware verification technique that performs a systematic, heuristics guided search of the state space of the model to be analyzed. It hence reconciles classical model checking technology with intelligent, heuristics driven search that has a long tradition in artificial intelligence, in particular in the area of action planning. The benefits are short or even optimally short error trails, in some instances a more efficient exploration of the state space, and the applicability of state space search in some application areas in which unintelligent search would not yield useful results. The seminar brought together researchers from the system verification and the artificial intelligence domain in order to discuss the current state of the art, and to elicit and discuss research challenges and future directions.
Cite as

Stefan Edelkamp, Stefan Leue, and Willem Visser. 06172 Executive Summary – Directed Model Checking. In Directed Model Checking. Dagstuhl Seminar Proceedings, Volume 6172, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{edelkamp_et_al:DagSemProc.06172.2,
  author =	{Edelkamp, Stefan and Leue, Stefan and Visser, Willem},
  title =	{{06172 Executive Summary – Directed Model Checking}},
  booktitle =	{Directed Model Checking},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6172},
  editor =	{Stefan Edelkamp and Stefan Leue and Willem Visser},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06172.2},
  URN =		{urn:nbn:de:0030-drops-9443},
  doi =		{10.4230/DagSemProc.06172.2},
  annote =	{Keywords: Model checking, heuristics, state space search, software and hardware verification}
}
Document
DOI: 10.4230/DagSemProc.06172.3
Efficient Software Model Checking of Data Structure Properties

Authors: Chandrasekhar Boyapati and Paul Darga

Abstract
This talk presents novel language and analysis techniques that significantly speed up software model checking of data structure properties. Consider checking a red-black tree implementation. Traditional software model checkers systematically generate all red-black tree states (within some given bounds) and check every red-black tree operation (such as insert, delete, or lookup) on every red-black tree state. Our key idea is as follows. As our checker checks a red-black tree operation $o$ on a red-black tree state $s$, it uses program analysis techniques to identify other red-black tree states $s'_1$, $s'_2$, ..., $s'_k$ on which the operation $o$ behaves similarly. Our analyses guarantee that if $o$ executes correctly on $s$, then $o$ will execute correctly on every $s'_i$. Our checker therefore does not need to check $o$ on any $s'_i$ once it checks $o$ on $s$. It thus safely prunes those state transitions from its search space, while still achieving complete test coverage within the bounded domain. Our preliminary results show {em orders of magnitude improvement} over previous approaches. We believe our techniques can make software model checking significantly faster, and thus enable checking of much larger programs and complex program properties than currently possible.
Cite as

Chandrasekhar Boyapati and Paul Darga. Efficient Software Model Checking of Data Structure Properties. In Directed Model Checking. Dagstuhl Seminar Proceedings, Volume 6172, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{boyapati_et_al:DagSemProc.06172.3,
  author =	{Boyapati, Chandrasekhar and Darga, Paul},
  title =	{{Efficient Software Model Checking of Data Structure Properties}},
  booktitle =	{Directed Model Checking},
  pages =	{1--19},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6172},
  editor =	{Stefan Edelkamp and Stefan Leue and Willem Visser},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06172.3},
  URN =		{urn:nbn:de:0030-drops-9450},
  doi =		{10.4230/DagSemProc.06172.3},
  annote =	{Keywords: Software Model Checking, Program Analysis, Linked Data Structures}
}

Filters

  • Authors
  • B
  • Boyapati, Chandrasekhar
  • D
  • Darga, Paul
  • E
  • Edelkamp, Stefan
  • L
  • Leue, Stefan
  • V
  • Visser, Willem

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