Checking properties of heap-manipulating procedures with a constraint solver
International Conference on Tools and Algorithms for the Construction and …, 2003•Springer
A method for finding bugs in object-oriented code is presented. It is capable of checking
complex user-defined structural properties—that is, of the configuration of objects on the
heap—and generates counterexample traces with no false alarms. It requires no annotation
beyond the specification to be checked, and is fully automatic. The method relies on a three-
step translation: from code to a formula in a first-order relational logic, then to a propositional
formula, and finally to conjunctive normal form. An off-the-shelf SAT solver is then used to …
complex user-defined structural properties—that is, of the configuration of objects on the
heap—and generates counterexample traces with no false alarms. It requires no annotation
beyond the specification to be checked, and is fully automatic. The method relies on a three-
step translation: from code to a formula in a first-order relational logic, then to a propositional
formula, and finally to conjunctive normal form. An off-the-shelf SAT solver is then used to …
Abstract
A method for finding bugs in object-oriented code is presented. It is capable of checking complex user-defined structural properties —that is, of the configuration of objects on the heap—and generates counterexample traces with no false alarms. It requires no annotation beyond the specification to be checked, and is fully automatic.
The method relies on a three-step translation: from code to a formula in a first-order relational logic, then to a propositional formula, and finally to conjunctive normal form. An off-the-shelf SAT solver is then used to find a solution that constitutes a counterexample.
This underlying scheme, presented previously, does not scale readily. In this paper, we show how a suite of optimizations results in much improved scalability. The optimizations are based on a special treatment of relations that are known to be functional, and target all steps. The effect of the optimizations is demonstrated by application to the analysis of a red-black tree implementation.
Springer