Underapproximating loops in C programs for fast counterexample detection (a.k.a. Unrolling is for chumps)

Matt Lewis ( University of Oxford )

Using algebraic techniques, we find closed forms for pieces of loops in C programs. We use those closed forms to rapidly find counterexamples to safety, even if those counterexamples take place after a large number of loop iterations. Our method is bit level accurate, can handle programs that manipulate arrays and pointers, does not generate false positives and can be integrated with existing software model checkers. We show experimental results that demonstrate the effectiveness of our approach for detecting buffer overflows in C programs.