Abstract
This paper addresses the problem of proving safety properties of imperative programs manipulating dynamically allocated data structures using destructive pointer updates. We present a new abstraction for linked data structures whose underlying graphs do not contain cycles. The abstraction is simple and allows us to decide reachability between dynamically allocated heap cells.
We present an efficient algorithm that computes the effect of low level heap mutations in the most precise way. The algorithm does not rely on the usage of a theorem prover. In particular, the worst case complexity of computing a single successor abstract state is O(V logV) where V is the number of program variables. The overall number of successor abstract states can be exponential in V. A prototype of the algorithm was implemented and is shown to be fast.
Our method also handles programs with “simple cycles” such as cyclic singly-linked lists, (cyclic) doubly-linked lists, and trees with parent pointers. Moreover, we allow programs which temporarily violate these restrictions as long as they are restored in loop boundaries.
Chapter PDF
Similar content being viewed by others
References
Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis by predicate abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 164–180. Springer, Heidelberg (2005)
Bingham, J., Rakamaric, Z.: A logic and decision procedure for predicate abstraction of heap-manipulating programs. Tech. Rep. TR-2005-19, Dept. of Comp. Sci., Univ. of BC, Canada (2005)
Bruns, G., Godefroid, P.: Generalized model checking: Reasoning about partial state spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 168–182. Springer, Heidelberg (2000)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Symp. on Princ. of Prog. Lang., pp. 269–282. ACM Press, New York (1979)
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, pp. 287–302. Springer, Heidelberg (2006)
Ghiya, R., Hendren, L.: Putting pointer analysis to work. In: Symp. on Princ. of Prog. Lang., ACM Press, New York (1998)
Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: CAV (1997)
Hendren, L.: Parallelizing Programs with Recursive Data Structures. PhD thesis, Cornell Univ., Ithaca, NY (January 1990)
Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: Verification via structure simulation. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 281–294. Springer, Heidelberg (2004)
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, vol. 4, pp. 102–131. Prentice-Hall, Englewood Cliffs (1981)
Klarlund, N., Møller, A.: MONA Version 1.4 User Manual. BRICS Notes Series NS-01-1, Dept. of Comp. Sci., Univ. of Aarhus (January 2001)
Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: POPL (2006)
Lee, O., Yang, H., Yi, K.: Automatic verification of pointer programs using grammar-based shape analysis. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 124–140. Springer, Heidelberg (2005)
Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 99–115. Springer, Heidelberg (2005)
Lev-Ami, T., Immerman, N., Sagiv, M.: Fast and precise abstraction for shape analysis. Technical Report TR-2006-01-001221, Tel-Aviv Univ.,(2006), Available at: http://www.cs.tau.ac.il/~tla/2006/papers/TR-2006-01-001221.pdf
Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Static Analysis Symp., pp. 280–301 (2000)
Manevich, R., Sagiv, M., Ramalingam, G., Field, J.: Partially disjunctive heap abstraction. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 265–279. Springer, Heidelberg (2004)
Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 181–198. Springer, Heidelberg (2005)
Reps, T., Loginov, A., Sagiv, M.: Semantic minimization of 3-valued propositional formulae. In: LICS, pp. 40–54 (2002)
Cananda Sable Research Group, McGill University. Soot: a java optimization framework, Available at: http://www.sable.mcgill.ca/soot/
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. Trans. on Prog. Lang. and Syst. (2002)
Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 530–545. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lev-Ami, T., Immerman, N., Sagiv, M. (2006). Abstraction for Shape Analysis with Fast and Precise Transformers. In: Ball, T., Jones, R.B. (eds) Computer Aided Verification. CAV 2006. Lecture Notes in Computer Science, vol 4144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817963_49
Download citation
DOI: https://doi.org/10.1007/11817963_49
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37406-0
Online ISBN: 978-3-540-37411-4
eBook Packages: Computer ScienceComputer Science (R0)