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 execu- tion traces that involve at most j heap cells and k loop itera- tions. This formula is conjoined with the negation of the pro- cedure’s specification. The models of the resulting formula, obtained using a constraint solver, are counterexamples: exe- cutions of the code that violate the specification. The method can analyze millions of executions in sec- onds, 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.