License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.06172.3
URN: urn:nbn:de:0030-drops-9450
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2007/945/
Go to the corresponding Portal

Boyapati, Chandrasekhar ; Darga, Paul

Efficient Software Model Checking of Data Structure Properties

pdf-format:
06172.BoyapatiChandrasekhar.Paper.945.pdf (0.4 MB)

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.


BibTeX - Entry

@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/opus/volltexte/2007/945},
  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