This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Modular Pluggable Analyses for Data Structure Consistency
December 2006 (vol. 32 no. 12)
pp. 988-1005
Hob is a program analysis system that enables the focused application of multiple analyses to different modules in the same program. In our approach, each module encapsulates one or more data structures and uses membership in abstract sets to characterize how objects participate in data structures. Each analysis verifies that the implementation of the module 1) preserves important internal data structure consistency properties and 2) correctly implements a set algebra interface that characterizes the effects of operations on the data structure. Collectively, the analyses use the set algebra to 1) characterize how objects participate in multiple data structures and to 2) enable the interanalysis communication required to verify properties that depend on multiple modules analyzed by different analyses. We implemented our system and deployed several pluggable analyses, including a flag analysis plug--in for modules in which abstract set membership is determined by a flag field in each object, a PALE shape analysis plug-in, and a theorem proving plug-in for analyzing arbitrarily complicated data structures. Our experience shows that our system can effectively 1) verify the consistency of data structures encapsulated within a single module and 2) combine analysis results from different analysis plug-ins to verify properties involving objects shared by multiple modules analyzed by different analyses.

[1] A. Møller and M.I. Schwartzbach, “The Pointer Assertion Logic Engine,” Programming Language Design and Implementation, 2001.
[2] M. Sagiv, T. Reps, and R. Wilhelm, “Parametric Shape Analysis via 3-Valued Logic,” ACM Trans. Program Languages and Systems, vol. 24, no. 3, pp. 217-298, 2002.
[3] T. Ball, R. Majumdar, T. Millstein, and S.K. Rajamani, “Automatic Predicate Abstraction of C programs,” Proc. ACM Programming Language Design and Implementation Conf. (PLDI), 2001.
[4] T.A. Henzinger, R. Jhala, R. Majumdar, and K.L. McMillan, “Abstractions from Proofs,” Proc. 31st Symp. Principles of Programming Languages, 2004.
[5] S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith, “Modular Verification of Software Components in C,” Proc. Int'l Conf. Software Eng. (ICSE '03), 2003.
[6] N. Bjørner, A. Browne, E. Chang, M. Colón, A. Kapur, Z. Manna, H.B. Sipma, and T.E. Uribe, “STeP: Deductive-Algorithmic Verification of Reactive and Real-Time systems,” Proc. Eighth Conf. Computer-Aided Verification, vol. 1102, pp. 415-418, 1996.
[7] M. Musuvathi, D.Y. Park, A. Chou, D.R. Engler, and D.L. Dill, “CMC: A Pragmatic Approach to Model Checking Real Code,” Proc. Symp. Operating Systems Design and Implementation (OSDI '02), 2002.
[8] C. Flanagan, K.R.M. Leino, M. Lilibridge, G. Nelson, J.B. Saxe, and R. Stata, “Extended Static Checking for Java,” Proc. ACM Conf. Programming Language Design and Implementation (PLDI), 2002.
[9] R.E. Strom and S. Yemini, “Typestate: A Programming Language Concept for Enhancing Software Reliability,” IEEE Trans. Software Eng., vol. 12, no. 1, Jan. 1986.
[10] R. DeLine and M. Fähndrich, “Enforcing High-Level Protocols in Low-Level Software,” Proc. ACM Programming Language Design and Implementation Conf. (PLDI), 2001.
[11] M. Fähndrich and K.R.M. Leino, “Heap Monotonic Typestates,” Proc. Int'l Workshop Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO), 2003.
[12] J. Field, D. Goyal, G. Ramalingam, and E. Yahav, “Typestate Verification: Abstraction Techniques and Complexity Results,” Proc. Int'l Symp. Static Analysis, 2003.
[13] M. Fahndrich and R. DeLine, “Adoption and Focus: Practical Linear Types for Imperative Programming,” Proc. ACM Programming Language Design and Implementation Conf. (PLDI), 2002.
[14] V. Kuncak, P. Lam, and M. Rinard, “Role Analysis,” Proc. Ann. ACM Symp. Principles of Programming Languages (POPL), 2002.
[15] P. Lam, V. Kuncak, and M. Rinard, “On Our Experience with Modular Pluggable Analyses,” Technical Report 965, Computer Science and Artifical Intelligence Laboratory (CSAIL), Massachusetts Inst. of Tech nology, Sept. 2004.
[16] P. Lam, V. Kuncak, and M. Rinard, “Hob: A Tool for Verifying Data Structure Consistency,” Proc. 14th Int'l Conf. Compiler Construction, tool demo, Apr. 2005.
[17] P. Lam, V. Kuncak, and M. Rinard, “Generalized Typestate Checking for Data Structure Consistency,” Proc. Sixth Int'l Conf. Verification, Model Checking and Abstract Interpretation, 2005.
[18] T. Nipkow, L.C. Paulson, and M. Wenzel, “Isabelle/HOL: A Proof Assistant for Higher-Order Logic,” Lecture Notes in Computer Science, vol. 2283. 2002.
[19] T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard, “Field Constraint Analysis,” Proc. Int'l Conf. Verification, Model Checking, and Abstract Interpretation, 2006.
[20] A. Podelski and T. Wies, “Boolean Heaps,” Proc. Int'l Static Analysis Symp., 2005.
[21] K. Zee, P. Lam, V. Kuncak, and M. Rinard, “Combining Theorem Proving with Static Analysis for Data Structure Consistency,” Proc. Int'l Workshop Software Verification and Validation (SVV '04), Nov. 2004.
[22] T. Wies, V. Kuncak, K. Zee, A. Podelski, and M. Rinard, “On Verifying Complex Properties Using Symbolic Shape Analysis,” Technical Report MPI-I-2006-2-1, Max-Planck Inst. for Computer Science, 2006
[23] P. Lam, V. Kuncak, and M. Rinard, “Cross-Cutting Techniques in Program Specification and Analysis,” Proc. Fourth Int'l Conf. Aspect-Oriented Software Development (AOSD '05), 2005.
[24] E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Design Patterns. Elements of Reusable Object-Oriented Software. Addison-Wesley, 1994.
[25] J.R. Büchi, “Weak Second-Order Arithmetic and Finite Automata,” Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, vol. 6, pp. 66-92, 1960.
[26] L. Loewenheim, “Über Mögligkeiten im Relativkalkül,” Mathematische Annalen, vol. 76, pp. 228-251, 1915.
[27] D. Jackson, I. Shlyakhter, and M. Sridharan, “A Micromodularity Mechanism,” Proc. ACM SIGSOFT Conf. Foundations of Software Eng./European Software Eng. Conf. (FSE/ESEC '01), 2001.
[28] A. Borgida, J. Mylopoulos, and R. Reiter, “On the Frame Problem in Procedure Specifications,” IEEE Trans. Software Eng., vol. 21, no. 10, pp. 785-798, Oct. 1995.
[29] D. Kozen, “Complexity of Boolean Algebras,” Theoretical Computer Science, vol. 10, pp. 221-247, 1980.
[30] B. Liskov and J. Guttag, Program Development in Java. Addison-Wesley, 2001.
[31] H. Jifeng, C.A.R. Hoare, and J.W. Sanders, “Data Refinement Refined,” Proc. European Symp. Programming (ESOP '86), 1986.
[32] P. Lam, V. Kuncak, K. Zee, and M. Rinard, “Set Interfaces for Generalized Typestate and Data Structure Consistency Verification,” Theoretical Computer Science, submitted.
[33] N. Klarlund and M.I. Schwartzbach, “Graph Types,” Proc. 20th ACM Symp. Principles of Programming Languages (POPL), 1993.
[34] J.W. Thatcher and J.B. Wright, “Generalized Finite Automata Theory with an Application to a Decision Problem of Second-Order Logic,” Math. Systems Theory, vol. 2, no. 1, pp. 57-81, Aug. 1968.
[35] N. Klarlund, A. Møller, and M.I. Schwartzbach, “MONA Implementation Secrets,” Proc. Fifth Int'l Conf. Implementation and Application of Automata, LNCS, 2000.
[36] N. Klarlund and A. Møller, MONA Version 1.4 User Manual, BRICS Notes Series NS-01-1, Dept. of Computer Science, Univ. of Aarhus, Jan. 2001.
[37] L. Stockmeyer and A.R. Meyer, “Cosmological Lower Bound on the Circuit Complexity of a Small Problem in Logic,” J. ACM, vol. 49, no. 6, pp. 753-784, 2002.
[38] E.W. Dijkstra, A Discipline of Programming. Prentice Hall, 1976.
[39] C. Flanagan and J.B. Saxe, “Avoiding Exponential Explosion: Generating Compact Verification Conditions,” Proc. 20th ACM Symp. Principles of Programming Languages (POPL), 2001.
[40] P. Lam, V. Kuncak, and M. Rinard, “Generalized Typestate Checking Using Set Interfaces and Pluggable Analyses,” SIGPLAN Notices, vol. 39, pp. 46-55, Mar. 2004.
[41] P. Cousot and R. Cousot, “Systematic Design of Program Analysis Frameworks,” Proc. 20th ACM Symp. Principles of Programming Languages (POPL), pp. 269-282, 1979.
[42] R.E. Strom and D.M. Yellin, “Extending Typestate Checking Using Conditional Liveness Analysis,” IEEE Trans. Software Eng., vol. 19, no. 5, May 1993.
[43] K. Bierhoff and J. Aldrich, “Lightweight Object Specification with Typestates,” Proc. European Software Eng. Conf./ACM SIGSOFT Symp. Foundations of Software Eng. (ESEC-FSE '05), pp. 217-226, Sept. 2005.
[44] V. Kuncak, “Modular Data Structure Verification,” PhD dissertation, Massachusetts Inst. of Technology, to appear, 2007.
[45] V. Kuncak, H.H. Nguyen, and M. Rinard, “An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic,” Proc. 20th Int'l Conf. Automated Deduction (CADE 20), July 2005.
[46] C.H. Papadimitriou, Computational Complexity. Addison-Wesley, 1994.
[47] V. Kuncak and M. Rinard, “An Overview of the Jahob Analysis System: Project Goals and Current Status,” Proc. NSF Next Generation Software Workshop, 2006.
[48] S. Drossopoulou, F. Damiani, M. Dezani-Ciancaglini, and P. Giannini, “Fickle: Dynamic Object Re-Classification,” Proc. 15th European Conf. Object-Oriented Programming (ECOOP), pp.130-149, 2001.
[49] S. Fink, E. Yahav, N. Dor, G. Ramalingam, and E. Geay, “Effective Typestate Verification in the Presence of Aliasing,” Proc. Int'l Symp. Software Testing and Analysis (ISSTA '06), 2006.
[50] T. Skolem, “Untersuchungen über die Axiome des Klassenkalküls and über ‘Produktations- und Summationsprobleme,’ welche gewisse Klassen von Aussagen betreffen,” Skrifter utgit av Vidnskapsselskapet i Kristiania, I. klasse, no. 3, 1919.
[51] V. Kuncak, H.H. Nguyen, and M. Rinard, “Deciding Boolean Algebra with Presburger Arithmetic,” J. Automated Reasoning, accepted for publication, 2006.
[52] D.R. Cheriton and M.E. Wolf, “Extensions for Multi-Module Records in Conventional Programming Languages,” Proc. ACM Programming Language Design and Implementation Conf. (PLDI), pp.296-306, 1987.
[53] G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C. Lopes, J. Loingtier, and J. Irwin, “Aspect-Oriented Programming,” Proc. 15th European Conf. Object-Oriented Programming (ECOOP), June 1997.
[54] V. Kuncak and K.R.M. Leino, “In-Place Refinement for Effect Checking,” Proc. Second Int'l Workshop Automated Verification of Infinite-State Systems (AVIS '03), Apr. 2003.
[55] P. O'Hearn, H. Yang, and J. Reynolds, “Separation and Information Hiding,” Proc. 20th ACM Symp. Principles of Programming Languages (POPL), pp. 268-280, 2004.
[56] R. Milner, M. Tofte, R. Harper, and D. MacQueen, The Definition of Standard ML (Revised). MIT Press, 1997.
[57] D.I. Good, R.L. Akers, and L.M. Smith, “Report on Gypsy 2.05,” technical report, Univ. of Texas at Austin, Feb. 1986.
[58] J.-R. Abrial, M.K.O. Lee, D. Neilson, P.N. Scharbach, and I. Sørensen, “The B-Method,” Proc. Fourth Int'l Symp. VDM Europe Formal Software Development, vol. 2, pp. 398-405, 1991.
[59] C.B. Jones, Systematic Software Development Using VDM. Prentice Hall Int'l Ltd., 1986.
[60] J. Woodcock and J. Davies, Using Z. Prentice Hall, 1996.
[61] J. Guttag and J. Horning, Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993.
[62] B. Dandanell, “Rigorous Development Using RAISE,” Proc. Conf. Software for Citical Systems, pp. 29-43, 1991.
[63] J.C. King, “A Program Verifier,” PhD dissertation, Carnegie Mellon Univ., 1970.
[64] G. Nelson, “Techniques for Program Verification,” technical report, XEROX Palo Alto Research Center, 1981.
[65] J.-C. Filliatre, “Verification of Non-Functional Programs Using Interpretations in Type Theory,” J. Functional Programming, vol. 13, no. 4, pp. 709-745, 2003.
[66] J.-C. Filliatre and C. Marchí, “Multi-Prover Verification of CPrograms,” Proc. Int'l Conf. Formal Eng. Methods (ICFEM '04), 2004.
[67] C. Marché, C. Paulin-Mohring, and X. Urbain, “The Krakatoa Tool for Certification of JAVA/JAVACARD Programs Annotated in JML,” J. Logic and Algebraic Programming, 2003.
[68] L. Burdy, Y. Cheon, D. Cok, M.D. Ernst, J. Kiniry, G.T. Leavens, K.R.M. Leino, and E. Poll, “An Overview of JML Tools and Applications,” Technical Report NII-R0309, Computing Science Inst., Univ. of Nijmegen, Mar. 2003.
[69] D.L. Detlefs, K.R.M. Leino, G. Nelson, and J.B. Saxe, “Extended Static Checking,” Technical Report 159, Compaq Systems Research Center, 1998.
[70] D. Detlefs, G. Nelson, and J.B. Saxe, “Simplify: A Theorem Prover for Program Checking,” Technical Report HPL-2003-148, Hewlett-Packard Laboratories Palo Alto, 2003.
[71] G. Nelson, “Verifying Reachability Invariants of Linked Structures,” Proc. ACM Symp. Principles of Programming Languages (POPL), 1983.
[72] T. Lev-Ami, N. Immerman, T. Reps, M. Sagiv, S. Srivastava, and G. Yorsh, “Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures,” Proc. 20th Int'l Conf. Automated Deduction (CADE 20), 2005.
[73] S.K. Lahiri and S. Qadeer, “Verifying Properties of Well-Founded Linked Lists,” Proc. ACM Symp. Principles of Programming Languages (POPL '06), 2006.
[74] D.R. Cok, “Reasoning with Specifications Containing Method Calls and Model Fields,” J. Object Technology, vol. 4, no. 8, pp. 77-103, Sept.-Oct. 2005.
[75] M. Barnett, R. DeLine, M. Fähndrich, K.R.M. Leino, and W. Schulte, “Verification of Object-Oriented Programs with Invariants,” J. Object Technology, vol. 3, no. 6, pp. 27-56, 2004.
[76] K.R.M. Leino and P. Müller, “A Verification Methodology for Model Fields,” Proc. European Symp. Programming (ESOP '06), 2006.
[77] T. Ball, S. Lahiri, and M. Musuvathi, “Zap: Automated Theorem Proving for Software Analysis, Technical Report MSR-TR-2005-137, Microsoft Research, 2005.
[78] S. Chaki, S.K. Rajamani, and J. Rehof, “Types as Models: Model Checking Message-Passing Programs,” Proc. 29th ACM SIGPLAN-SIGACT Principles of Programming Languages (POPL), pp. 45-57, 2002.
[79] P. Meunier, R.B. Findler, and M. Felleisen, “Modular Set-Based Analysis from Contracts,” Proc. 33rd ACM Principles of Programming Languages (POPL), pp. 218-231, Jan. 2006.
[80] B.-Y.E. Chang and K.R.M. Leino, “Abstract Interpretation with Alien Expressions and Heap Structures,” Proc. Conf. Verification, Model Checking and Abstract Interpretation (VMCAI' 05), Jan. 2005.

Index Terms:
Typestate, data structure, invariant, program analysis, program verification, shape analysis, formal methods, programming language design.
Citation:
Viktor Kuncak, Patrick Lam, Karen Zee, Martin C. Rinard, "Modular Pluggable Analyses for Data Structure Consistency," IEEE Transactions on Software Engineering, vol. 32, no. 12, pp. 988-1005, Dec. 2006, doi:10.1109/TSE.2006.125
Usage of this product signifies your acceptance of the Terms of Use.