Efficient Software Model Checking of Data Structure Properties

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.