Abstract
Programs commonly maintain multiple linked data structures. Correlations between multiple data structures may often be non-existent or irrelevant to verifying that the program satisfies certain safety properties or invariants. In this paper, we show how this independence between different (singly-linked) data structures can be utilized to perform shape analysis and verification more efficiently. We present a new abstraction based on decomposing graphs into sets of subgraphs, and show that, in practice, this new abstraction leads to very little loss of precision, while yielding substantial improvements to efficiency.
Chapter PDF
References
Chase, D.R., Wegman, M., Zadeck, F.: Analysis of pointers and structures. In: Proc. Conf. on Prog. Lang. Design and Impl., ACM Press, New York (1990)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, California, ACM Press, New York (1977)
Distefano, D., O’Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, Springer, Heidelberg (2006)
Garey, M.R., Johnson, D.S.: Computers and Intractability, A Guide to the Theory of NP-Completeness. W.H. Freeman and Company, New York (1979)
Gotsman, A., Berdine, J., Cook, B.: Interprocedural shape analysis with separated heap abstractions. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 240–260. Springer, Heidelberg (2006)
Hackett, B., Rugina, R.: Region-based shape analysis with tracked locations. In: Proc. Symp. on Principles of Prog. Languages (2005)
Jones, N.D., Muchnick, S.S.: Complexity of flow analysis, inductive assertion synthesis, and a language due to dijkstra. In: Program Flow Analysis: Theory and Applications, Prentice-Hall, Englewood Cliffs (1981)
Jones, N.D., Muchnick, S.S.: Flow analysis and optimization of Lisp-like structures. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications, Prentice-Hall, Englewood Cliffs (1981)
Sagiv, M., Immerman, N., Lev-Ami, T.: Abstraction for Shape Analysis with Fast and Precise Transformers. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 547–561. Springer, Heidelberg (2006)
Sagiv, M., Lev-Ami, T.: TVLA: A System for Implementing Static Analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 280–302. Springer, Heidelberg (2000)
Manevich, R., et al.: Shape analysis by graph decomposition (2006), A full version of this paper is available at http://www.cs.tau.ac.il/~rumster/sagd.full.pdf
Manevich, R., et al.: Partially disjunctive heap abstraction. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, Springer, Heidelberg (2004)
Manevich, R., et al.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, Springer, Heidelberg (2005)
Rinetzky, N., et al.: A semantics for procedure local heaps and its abstractions. In: 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’05) (2005)
Sagiv, M., Rinetzky, N., Yahav, E.: Interprocedural Shape Analysis for Cutpoint-Free Programs. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 284–302. Springer, Heidelberg (2005)
Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems 20(1) (1998)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems (2002)
Yahav, E., Ramalingam, G.: Verifying safety properties using separation and heterogeneous abstractions. In: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, Washington DC, USA, pp. 25–34. ACM Press, New York (2004), doi:10.1145/996841.996846
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Manevich, R., Berdine, J., Cook, B., Ramalingam, G., Sagiv, M. (2007). Shape Analysis by Graph Decomposition. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)