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-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Vaziri, M., & Jackson, D. (2003). Checking properties of heap-manipulating procedures with a constraint solver. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2619, 505–520. https://doi.org/10.1007/3-540-36577-x_37
Mendeley helps you to discover research relevant for your work.