Efficient Software Model Checking of Data Structure Properties

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\u27_1$, $s\u27_2$, ..., $s\u27_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\u27_i$. Our checker therefore does not need to check $o$ on any $s\u27_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