title: Under-approximating loops in C programs for fast counterexample detection.
abstract: Many software model checkers only detect counterexamples with deep loops after exploring numerous spurious and increasingly longer counterexamples. We propose a technique that aims at eliminating this weakness by constructing auxiliary paths that represent the effect of a range of loop iterations. Unlike acceleration, which captures the exact effect of arbitrarily many loop iterations, these auxiliary paths may under-approximate the behaviour of the loops. In return, the approximation is sound with respect to the bit-vector semantics of programs. Our approach supports arbitrary conditions and assignments to arrays in the loop body, but may as a result introduce quantified conditionals. To reduce the resulting performance penalty, we present two quantifier elimination techniques specially geared towards our application. Loop under-approximation can be combined with a broad range of verification techniques. We paired our techniques with lazy abstraction and bounded model checking, and evaluated the resulting tool on a number of buffer overflow benchmarks, demonstrating its ability to efficiently detect deep counterexamples in C programs that manipulate arrays.
authors.affiliation: University of Oxford, Oxford, UK.
authors.forename: Daniel
authors.initials: D
authors.lastname: Kroening
authors.affiliation: University of Oxford, Oxford, UK.
authors.forename: Matt
authors.initials: M
authors.lastname: Lewis
authors.affiliation: Vienna University of Technology, Vienna, Austria.
authors.forename: Georg
authors.initials: G
authors.lastname: Weissenbacher
keywords: Counterexamples; Loop acceleration; Model checking; Underapproximation