When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.06172.3
URN: urn:nbn:de:0030-drops-9450
Go to the corresponding Portal

Boyapati, Chandrasekhar ; Darga, Paul

Efficient Software Model Checking of Data Structure Properties

06172.BoyapatiChandrasekhar.Paper.945.pdf (0.4 MB)


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.

BibTeX - Entry

  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 =		{},
  URN =		{urn:nbn:de:0030-drops-9450},
  doi =		{10.4230/DagSemProc.06172.3},
  annote =	{Keywords: Software Model Checking, Program Analysis, Linked Data Structures}

Keywords: Software Model Checking, Program Analysis, Linked Data Structures
Collection: 06172 - Directed Model Checking
Issue Date: 2007
Date of publication: 22.03.2007

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI