This paper describes the Corral tool for finding bugs in device drivers using a variant of bounded model checking. Like many bounded model checkers, they inline all functions and unroll all loops up to some bound – increasing the bound until some limit or until a bug is found. What is interesting is that, instead of inlining all functions at once, they incrementally inline functions according to some heuristics. They also use a CEGAR-like mechanism to control variable abstraction.
What I like about this paper is the discussion of several heuristics, improvements, tricks, etc. that they use to get performance. For example, when searching for the minimal number of variables in the abstraction, they could generate N different verification conditions VC and try each one. Instead, they generate a single VC with additional Boolean variables to enable/disable use of each variable. They then invoke the SMT solver N times on a single VC - potentially benefiting from anything that the solver learns that applies across multiple solutions efforts.