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.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
A. Andoni, D. Daniliuc, S. Khurshid, and D. Marinov. “Evaluating the Small Scope Hypothesis”, MIT Laboratory for Computer Science, September 2002. Unpublished manuscript.
T. Ball, S. K. Rajamani. “The SLAM Project: Debugging System Software via Static Analysis”, Proc. POPL 2002, January 2002.
D. R. Chase, M. Wegman and F. Zadeck. “Analysis of Pointers and Structures”, Proc. Conf. on Programming Language Design and Implementation, 1990.
J. C. Corbett, M. B. Dwyer, J. Hatcli., S. Laubach, C. S. Pasareanu, Robby, H. Zheng. “Bandera: Extracting Finite-State Models from Java Source Code”, Proc. International Conference on Software Engineering, June 2000.
T. H. Cormen, C. E. Leiserson, R. L. Rivest. “Introduction to Algorithms”, MIT Press, 1990.
D. Detlefs, K. R. Leino, G. Nelson, and J. Saxe. “Extended Static Checking”. Technical Report 159, Compaq Systems Research Center, 1998.
Cormac Flanagan. Personal communication.
E. Goldberg and Y. Novikov. “BerkMin: A fast and robust SAT-solver”, In Design, Automation, and Test in Europe, March 2002.
G.J. Holzmann. “The Model Checker Spin”, IEEE Trans. on Software Engineering, Vol. 23, 5, May 1997.
G. J. Holzmann and M. H. Smith. “Automating Software Feature Verification”, Bell Labs Technical Journal, Vol. 5, 2, April-June 2000.
Daniel Jackson. “Automating First-Order Relational Logic”, Proc. ACM SIGSOFT Conf. Foundations of Software Engineering, San Diego, November 2000.
D. Jackson, I. Shlyakhter and M. Sridharan. “A Micromodularity Mechanism”, Proc. ACM SIGSOFT Conf. Foundations of Software Engineering, 2001.
D. Jackson and M. Vaziri. “Finding Bugs with a Constraint Solver”, Proc. International Conference on Software Testing and Analysis, August 2000.
R. Manevich, G. Ramalingam, J. Field, D. Goyal, M. Sagiv. “Compactly Representing First-Order Structures for Static Analysis”, In Proc. SAS 2002, 2002.
D. A. Plaisted and S. Greenbaum. “A Structure-Preserving Clause Form Translation”, Journal of Symbolic Computation, 2:293–304, 1986.
M. Sagiv, T. Reps, and R. Wilhelm. “Parametric shape analysis via 3-valued logic”, In ACM Transactions on Programming Languages and Systems, 24(3), 217–298, 2002.
W. Visser, K. Havelund, G. Brat and S. Park. “Model Checking Programs”, International Conference on Automated Software Engineering, September 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vaziri, M., Jackson, D. (2003). Checking Properties of Heap-Manipulating Procedures with a Constraint Solver. In: Garavel, H., Hatcliff, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2003. Lecture Notes in Computer Science, vol 2619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36577-X_37
Download citation
DOI: https://doi.org/10.1007/3-540-36577-X_37
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00898-9
Online ISBN: 978-3-540-36577-8
eBook Packages: Springer Book Archive