Advertisement

Constructing Specialized Shape Analyses for Uniform Change

  • Tal Lev-Ami
  • Mooly Sagiv
  • Neil Immerman
  • Thomas Reps
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4349)

Abstract

This paper is concerned with one of the basic problems in abstract interpretation, namely, for a given abstraction and a given set of concrete transformers (that express the concrete semantics of a program), how does one create the associated abstract transformers? We develop a new methodology for addressing this problem, based on a syntactically restricted language for expressing concrete transformers. We use this methodology to produce best abstract transformers for abstractions of many important data structures.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL (1979)Google Scholar
  2. 2.
    Immerman, N.: Descriptive Complexity. Springer, Heidelberg (1999)zbMATHGoogle Scholar
  3. 3.
    Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. Trans. on Prog. Lang. and Syst. (2002)Google Scholar
  4. 4.
    Loginov, A., Reps, T., Sagiv, M.: Abstraction refinement via inductive learning. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, Springer, Heidelberg (2005)Google Scholar
  5. 5.
    Dong, G., Su, J.: Incremental and decremental evaluation of transitive closure by first-order queries. Inf. & Comput. 120, 101–106 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Hesse, W.: Dynamic Computational Complexity. PhD thesis, Department of Computer Science, UMass, Amherst (2003)Google Scholar
  7. 7.
    Rakamaric, Z., Bingham, J., Hu, A.: A better logic and decision procedure for predicate abstraction of heap-manipulating programs. Tech. Rep. TR-2006-02, Dept. of Comp. Sci. Univ. of BC, Canada (2006)Google Scholar
  8. 8.
    Lev-Ami, T., et al.: Constructing specialized shape analyses for uniform change. Technical Report TR-2006-11-01, Tel-Aviv Univ (2006), http://www.cs.tau.ac.il/~tla/2006/papers/TR-2006-11-01.pdf
  9. 9.
    Manevich, R., et al.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 181–198. Springer, Heidelberg (2005)Google Scholar
  10. 10.
    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)Google Scholar
  11. 11.
    Lev-Ami, T., Immerman, N., Sagiv, M.: Abstraction for shape analysis with fast and precise transformers. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 533–546. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    Myers, E.: Efficient applicative data types. In: POPL, pp. 66–75 (1984)Google Scholar
  13. 13.
    Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, New York (1998)Google Scholar
  14. 14.
    Brown, A.L.: Persistent Object Stores. Univ. of St Andrews (1989)Google Scholar
  15. 15.
    Edmonds, J., Johnson, E.L.: Matching, Euler tours and the chinese postman. Mathematical Programming 5, 88–124 (1973)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    Hendren, L.: Parallelizing Programs with Recursive Data Structures. PhD thesis, Cornell Univ. Ithaca (1990)Google Scholar
  17. 17.
    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)CrossRefGoogle Scholar
  18. 18.
    Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol. 2618, Springer, Heidelberg (2003)CrossRefGoogle Scholar
  19. 19.
    Loginov, A.: Refinement-based program verification via three-valued-logic analysis. PhD thesis, Comp. Sci. Dept. Univ. of Wisconsin, Madison (2006)Google Scholar
  20. 20.
    Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Formal Descriptions of Programming Concepts, pp. 237–277 (1978)Google Scholar
  21. 21.
    Rinetzky, N., Sagiv, M., 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)CrossRefGoogle Scholar
  22. 22.
    Nelson, G.: Verifying reachability invariants of linked structures. In: POPL, pp. 38–47 (1983)Google Scholar
  23. 23.
    Møller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: PLDI, pp. 221–231(2001)Google Scholar
  24. 24.
    Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: POPL (2006)Google Scholar
  25. 25.
    Lev-Ami, T., et al.: Simulating reachability using first-order logic with applications to verification of linked data structures. In: Nieuwenhuis, R. (ed.) Automated Deduction – CADE-20. LNCS (LNAI), vol. 3632, pp. 99–115. Springer, Heidelberg (2005)Google Scholar
  26. 26.
    Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) Model Checking Software. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  27. 27.
    Henzinger, T.A., et al.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) Model Checking Software. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  28. 28.
    Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, Springer, Heidelberg (2004)Google Scholar
  29. 29.
    Rabin, M.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141, 1–35 (1969)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Tal Lev-Ami
    • 1
  • Mooly Sagiv
    • 1
  • Neil Immerman
    • 2
  • Thomas Reps
    • 3
  1. 1.School of Computer Science, Tel Aviv University 
  2. 2.Department of Computer Science, UMass, Amherst 
  3. 3.Computer Science Department, University of Wisconsin, Madison 

Personalised recommendations