Compactly Representing First-Order Structures for Static Analysis

  • R. Manevich
  • G. Ramalingam
  • J. Field
  • D. Goyal
  • M. Sagiv
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2477)


A fundamental bottleneck in applying sophisticated static analyses to large programs is the space consumed by abstract program states. This is particularly true when analyzing programs that make extensive use of heap-allocated data. The TVLA Three-Valued Logic Analysis) program analysis and verification system models dynamic allocation precisely by representing program states as first-order structures. In such a representation, a finite collection of predicates is used to define states; the predicates range over a universe of individuals that may evolve—expand and contract—during analysis. Evolving first-order structures can be used to encode a wide variety of analyses, including most analyses whose abstract states are represented by directed graphs or maps. This paper addresses the problem of space consumption in such analyses by describing and evaluating two novel structure representation techniques. One technique uses ordered binary decision diagrams (OB-DDs); the other uses a variant of a functional map data structure. Using a suite of benchmark analysis problems, we systematically compare the new representations with TVLA’s existing state representation. The results show that both the OBDD and functional implementations reduce space consumption in TVLA by a factor of 4 to 10 relative to the current TVLA state representation, without compromising analysis time. In addition to TVLA, we believe that our results are applicable to many program analysis systems that represent states as graphs, maps, or other structures of similar complexity.


Boolean Variable Abstract Interpretation Binary Decision Diagram Mutable Structure Program Point 
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.
    A. Appel and M. Ginsburg. Modern Compiler Implementation in C. Cambridge University Press, New York, Cambridge, 1998.Google Scholar
  2. 2.
    R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. A CM Computing Surveys, 24(3):293–318, Sept. 1992.Google Scholar
  3. 3.
    L. Cardelli and A. Gordon. Mobile ambients. In M. Nivat, editor, Proc. of Foundations of Software Science and Computation Structures (FoSSaCS), volume 1378 of LNCS, pages 140–155. Springer-Verlag, Mar. 1998.CrossRefGoogle Scholar
  4. 4.
    N. Dor, M. Rodeh, and M. Sagiv. Checking cleanness in linked lists. In Proc. Static Analysis Symp., pages 115–134, July 2000.Google Scholar
  5. 5.
    N. Klarlund, A. Moller, and M. I. Schwartzbach. MONA implementation secrets. In CIAA, pages 182–194, 2000.Google Scholar
  6. 6.
    T. Lev-Ami and M. Sagiv. TVLA: A framework for Kleene based static analysis. In J. Palsberg, editor, Proc. Static Analysis Symp., volume 1824 of Lecture Notes in Computer Science, pages 280–301. Springer-Verlag, 2000. Scholar
  7. 7.
    F. Martin. PAG-an efficient program analyzer generator. International Journal on Software Tools for Technology Transfer, 2(1):46–67, 1998.zbMATHCrossRefGoogle Scholar
  8. 8.
    L. Mauborgne. Abstract interpretation using typed decision graphs. Science of Computer Programming, 31(1):91–112, May 1998.Google Scholar
  9. 9.
    Microsoft Research. The SLAM project., 2001.
  10. 10.
    F. Nielson, H. Nielson, and M. Sagiv. A Kleene analysis of mobile ambients. In G. Smolka, editor, Proc. of ESOP 2000, volume 1782 of LNCS, pages 305–319. Springer, 2000.Google Scholar
  11. 11.
    G. Ramalingam, A. Warshavsky, J. Field, D. Goyal, and M. Sagiv. Deriving specialized program analyses for certifying component-client conformance. In Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, pages 83–94, Berlin, June 2002.Google Scholar
  12. 12.
    T. Reps, M. Sagiv, and R. Wilhelm. Automatic verification of a simple mark and sweep garbabge collector. Presented in the 2001 University of Washington and Microsoft Research Summer Institute, Specifying and Checking Properties of Software,, 2001.
  13. 13.
    M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In Proc. ACM Symp. on Principles of Programming Languages, pages 105–118, 1999.Google Scholar
  14. 14.
    S. Sagiv, N. Francez, M. Rodeh, and R. Wilhelm. A logic-based approach to data flow analysis problems. Acta Inf., 35(6):457–504, June 1998.Google Scholar
  15. 15.
    F. Somenzi. Colorado University Decision Diagram Package (CUDD). Department of Electrical and Computer Engineering, University of Colorado at Boulder, 1998.
  16. 16.
    H. Veith. How to encode a logical structure by an OBDD. In IEEE Conference on Computational Complexity, pages 122–131, 1998.Google Scholar
  17. 17.
    E. Yahav. Verifying safety properties of concurrent Java programs using 3-valued logic. In Proc. ACM Symp. on Principles of Programming Languages, pages 27–40, 2001.Google Scholar
  18. 18.
    B. Yang, R. E. Bryant, D. R. O’Hallaron, A. Biere, O. Coudert, G. Janssen, R. K. Ranjan, and F. Somenzi. A performance study of BDD-based model checking. In Proceedings of the Formal Methods on Computer-Aided Design, pages 255–289, November 1998.Google Scholar
  19. 19.
    T. Yavuz-Kahveci, M. Tuncer, and T. Bultan. Composite symbolic library. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of Lecture Notes in Computer Science, pages 335–344. Springer-Verlag, April 2001.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • R. Manevich
    • 1
  • G. Ramalingam
    • 2
  • J. Field
    • 2
  • D. Goyal
    • 2
  • M. Sagiv
    • 1
  1. 1.Tel Aviv UniversityIsrael
  2. 2.IBM T.J. Watson Research CenterUSA

Personalised recommendations