Search Results

Documents authored by Darga, Paul


Document
Efficient Software Model Checking of Data Structure Properties

Authors: Chandrasekhar Boyapati and Paul Darga

Published in: Dagstuhl Seminar Proceedings, Volume 6172, Directed Model Checking (2007)


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}
}
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