License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-9450
URL: http://drops.dagstuhl.de/opus/volltexte/2007/945/

Boyapati, Chandrasekhar ; Darga, Paul

Efficient Software Model Checking of Data Structure Properties

pdf-format:
Dokument 1.pdf (364 KB)


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:DSP:2007:945,
  author =	{Chandrasekhar Boyapati and Paul Darga},
  title =	{Efficient Software Model Checking of Data Structure Properties},
  booktitle =	{Directed Model Checking},
  year =	{2007},
  editor =	{Stefan Edelkamp and Stefan Leue and Willem Visser},
  number =	{06172},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2007/945},
  annote =	{Keywords: Software Model Checking, Program Analysis, Linked Data Structures}
}

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


DROPS-Home | Fulltext Search | Imprint Published by LZI