Efficient Software Model Checking of Data Structure Properties

This paper 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 s1, s2, ..., sk on which the operation o behaves similarly. Our analyses guarantee that if o executes correctly on s, then o will execute correctly on every si. Our checker therefore does not need to check o on any si 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 resu...

• Type: Conference
• Year: 2006
• Where: DAGSTUHL
• Authors: Chandrasekhar Boyapati, Paul T. Darga
• Keywords: DAGSTUHL 2006, DAGSTUHL 2007, Red-black Tree, Red-black Tree Operation, Red-black Tree States