Finding bugs with a constraint solver

Abstract

A method for finding bugs in code is presented. For given small numbers j and k, the code of a procedure is translated into a relational formula whose models represent all execution traces that involve at most j heap cells and k loop iterations. This formula is conjoined with the negation of the procedure's specification. The models of the resulting formula, obtained using a constraint solver, are counterexamples: executions of the code that violate the specification. The method can analyze millions of executions in seconds, and thus rapidly expose quite subtle flaws. It can accommodate calls to procedures for which specifications but no code is available. A range of standard properties (such as absence of null pointer dereferences) can also be easily checked, using predefined specifications.