Verifying Pointer and String Analyses with Region Type Systems

  • Lennart Beringer
  • Robert Grabowski
  • Martin Hofmann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6355)


Pointer analysis statically approximates the heap pointer structure during a program execution in order to track heap objects or to establish alias relations between references, and usually contributes to other analyses or code optimizations. In recent years, a number of algorithms have been presented that provide an efficient, scalable, and yet precise pointer analysis. However, it is unclear how the results of these algorithms compare to each other semantically.

In this paper, we present a general region type system for a Java-like language and give a formal soundness proof. The system is subsequently specialized to obtain a platform for embedding the results of various existing context-sensitive pointer analysis algorithms, thereby equipping the computed relations with a common interpretation and verification. We illustrate our system by outlining an extension to a string value analysis that builds on pointer information.


Type System Call Graph Abstraction Principle String Analysis Program Language Design 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Emami, M., Ghiya, R., Hendren, L.J.: Context-sensitive interprocedural points-to analysis in the presence of function pointers. In: 1994 Conference on Programming Language Design and Implementation (PLDI 1994), pp. 242–256. ACM, New York (1994)Google Scholar
  2. 2.
    Andersen, L.O.: Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen (1994)Google Scholar
  3. 3.
    Steensgaard, B.: Points-to analysis in almost linear time. In: 23rd Symposium on Principles of Programming Languages (POPL 1996), pp. 32–41. ACM, New York (1996)Google Scholar
  4. 4.
    Berndl, M., Lhoták, O., Qian, F., Hendren, L., Umanee, N.: Points-to analysis using BDDs. In: 2003 Conference on Programming Language Design and Implementation (PLDI 2003). ACM, New York (2003)Google Scholar
  5. 5.
    Bravenboer, M., Smaragdakis, Y.: Strictly declarative specification of sophisticated points-to analyses. In: 24th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2009), pp. 243–262. ACM, New York (2009)Google Scholar
  6. 6.
    Igarashi, A., Pierce, B., Wadler, P.: Featherweight Java: A minimal core calculus for Java and GJ. In: 1999 Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 1999). ACM, New York (1999)Google Scholar
  7. 7.
    Ryder, B.G.: Dimensions of precision in reference analysis of object-oriented programming languages. In: Hedin, G. (ed.) CC 2003. LNCS, vol. 2622, pp. 126–137. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  8. 8.
    Christensen, A.S., Møller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 9.
    Crégut, P., Alvarado, C.: Improving the Security of Downloadable Java Applications With Static Analysis. Electronic Notes in Theoretical Computer Science 141(1), 129–144 (2005)CrossRefGoogle Scholar
  10. 10.
    Shivers, O.: Control-Flow Analysis of Higher-Order Languages, or Taming Lambda. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA, Technical Report CMU-CS-91-145 (1991)Google Scholar
  11. 11.
    Banerjee, A., Jensen, T.: Modular control-flow analysis with rank 2 intersection types. Mathematical Structures in Computer Science 13(1), 87–124 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Hardekopf, B., Lin, C.: Semi-sparse flow-sensitive pointer analysis. SIGPLAN Not. 44(1), 226–238 (2009)CrossRefzbMATHGoogle Scholar
  13. 13.
    Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: 15th Symposium on Principles of Programming Languages (POPL 1988), pp. 47–57. ACM, New York (1988)Google Scholar
  14. 14.
    Benton, N., Kennedy, A., Beringer, L., Hofmann, M.: Relational semantics for effect-based program transformations with dynamic allocation. In: Principles and Practice of Decl. Prog. (PPDP 2007). ACM, New York (2007)Google Scholar
  15. 15.
    Tofte, M., Talpin, J.P.: Region-based memory management. Information and Computation 132(2), 109–176 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Crary, K., Walker, D., Morrisett, G.: Typed memory management in a calculus of capabilities. In: 26th Symposium on Principles of Programming Languages (POPL 1999), pp. 262–275. ACM, New York (1999)Google Scholar
  17. 17.
    Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: 2002 Conference on Programming Language Design and Implementation (PLDI 2002), pp. 1–12. ACM, New York (2002)Google Scholar
  18. 18.
    Lhoták, O.: Program Analysis using Binary Decision Diagrams. PhD thesis, McGill University (January 2006)Google Scholar
  19. 19.
    Lenherr, T.: Taxonomy and Applications of Alias Analysis. Master’s thesis, ETH Zürich (2008)Google Scholar
  20. 20.
    Hofmann, M., Jost, S.: Type-based amortised heap-space analysis. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 22–37. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  21. 21.
    Beringer, L., Grabowski, R., Hofmann, M.: Verifying Pointer and String Analyses with Region Type Systems: Soundness proofs and other material (2010),
  22. 22.
    Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)zbMATHGoogle Scholar
  23. 23.
    Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications. Prentice Hall International, Englewood Cliffs (1981)Google Scholar
  24. 24.
    Milanova, A., Rountev, A., Ryder, B.G.: Parameterized object sensitivity for points-to analysis for Java. ACM Trans. Softw. Eng. Methodol. 14(1), 1–41 (2005)CrossRefGoogle Scholar
  25. 25.
    Whaley, J., Lam, M.S.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. SIGPLAN Not. 39(6), 131–144 (2004)CrossRefGoogle Scholar
  26. 26.
    Nystrom, E.M., Kim, H.S., Hwu, W.W.: Importance of heap specialization in pointer analysis. In: 5th Workshop on Program Analysis for Software Tools and Engineering (PASTE 2004). ACM, New York (2004)Google Scholar
  27. 27.
    Tripp, O., Pistoia, M., Fink, S.J., Sridharan, M., Weisman, O.: Taj: effective taint analysis of web applications. In: 2009 Conference on Programming Language Design and Implementation (PLDI 2009), pp. 87–97. ACM, New York (2009)CrossRefGoogle Scholar
  28. 28.
    Beringer, L., Hofmann, M., Pavlova, M.: Certification Using the Mobius Base Logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 25–51. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  29. 29.
    Barthe, G., Pichardie, D., Rezk, T.: A certified lightweight non-interference Java bytecode verifier. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 125–140. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  30. 30.
    Diwan, A., McKinley, K.S., Moss, J.E.B.: Type-based alias analysis. In: 1998 Conference on Programming Language Design and Implementation (PLDI 1998), pp. 106–117. ACM, New York (1998)Google Scholar
  31. 31.
    Loncaric, S.: A survey of shape analysis techniques. Pattern Recognition 31, 983–1001 (1998)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Lennart Beringer
    • 1
  • Robert Grabowski
    • 2
  • Martin Hofmann
    • 2
  1. 1.Department of Computer SciencePrinceton UniversityPrincetonUSA
  2. 2.Institut für InformatikLudwig-Maximilians-UniversitätMünchenGermany

Personalised recommendations