Abstract
We present an analysis to verify abstract set specifications for programs that use object field values to determine the membership of objects in abstract sets. In our approach, each module may encapsulate several data structures and use membership in abstract sets to characterize how objects participate in its data structures. Each module’s specification uses set algebra formulas to characterize the effects of its operations on the abstract sets. The program may define abstract set membership in a variety of ways; arbitrary analyses (potentially with multiple analyses applied to different modules in the same program) may verify the corresponding set specifications. The analysis we present in this paper verifies set specifications by constructing and verifying set algebra formulas whose validity implies the validity of the set specifications.
We have implemented our analysis and annotated several programs (75-2500 lines of code) with set specifications. We found that our original analysis algorithm did not scale; this paper describes several optimizations that improve the scalability of our analysis. It also presents experimental data comparing the original and optimized versions of our analysis.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proc. ACM PLDI (2001)
Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 158. Springer, Heidelberg (2002)
Blume, W., Eigenmann, R.: Performance analysis of parallelizing compilers on the Perfect Benchmarks programs. IEEE Transactions on Parallel and Distributed Systems 3(6), 643–656 (1992)
Clarke, L., Richardson, D.: Symbolic evaluation methods for program analysis. In: Program Flow Analysis: Theory and Applications, ch. 9. Prentice-Hall, Inc., Englewood Cliffs (1981)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. 6th POPL, San Antonio, Texas, pp. 269–282. ACM Press, New York (1979)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the 5th POPL, Tucson, Arizona, pp. 84–97. ACM Press, New York (1978)
DeLine, R., Fähndrich, M.: Enforcing high-level protocols in low-level software. In: Proc. ACM PLDI (2001)
DeLine, R., Fähndrich, M.: Typestates for objects. In: Proc. 18th ECOOP (June 2004)
Drossopoulou, S., Damiani, F., Dezani-Ciancaglini, M., Giannini, P.: Fickle: Dynamic object re-classification. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 130–149. Springer, Heidelberg (2001)
Fahndrich, M., DeLine, R.: Adoption and focus: Practical linear types for imperative programming. In: Proc. ACM PLDI (2002)
Fähndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an objectoriented language. In: Proceedings of the 18th ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, pp. 302–312. ACM Press, New York (2003)
Fähndrich, M., Leino, K.R.M.: Heap monotonic typestates. In: International Workshop on Aliasing, Confinement and Ownership in object-oriented programming, IWACO (2003)
Field, J., Goyal, D., Ramalingam, G., Yahav, E.: Typestate verification: Abstraction techniques and complexity results. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694. Springer, Heidelberg (2003)
Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: Generating compact verification conditions. In: Proc. 28th ACM POPL (2001)
Gamma, E., Helm, R., Johnson, R., Vlisside, J.: Design Patterns. Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1994)
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: 31st POPL (2004)
Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A relational approach to interprocedural shape analysis. In: 11th SAS (2004)
Klarlund, N., Møller, A.: MONA Version 1.4 User Manual. BRICS Notes Series NS-01-1, Department of Computer Science, University of Aarhus (January 2001)
Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Proc. 5th International Conference on Implementation and Application of Automata. LNCS, vol. 2000 (2001)
Kozen, D.: Complexity of boolean algebras. Theoretical Computer Science 10, 221–247 (1980)
Kuncak, V., Lam, P., Rinard, M.: Role analysis. In: Proc. 29th POPL (2002)
Kuncak, V., Rinard, M.: The first-order theory of sets with cardinality constraints is decidable. Technical Report 958, MIT CSAIL (July 2004)
Lam, P., Kuncak, V., Rinard, M.: Generalized Typestate Checking for Data Structure Consistency 447. On our experience with modular pluggable analyses. Technical Report 965, MIT CSAIL (September 2004)
Lam, P., Kuncak, V., Zee, K., Rinard, M.: The Hob project web page (2004), http://cag.csail.mit.edu/~plam/hob/
Leino, K.R.M.: Efficient weakest preconditions. KRML114a (2003)
Loewenheim, L.: Über mögligkeiten im relativkalkül. Math. Annalen 76, 228–251 (1915)
Møller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Proc. ACM PLDI (2001)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS 24(3), 217–298 (2002)
Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis problems. In: Program Flow Analysis: Theory and Applications. Prentice-Hall, Inc., Englewood Cliffs (1981)
Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability, January. IEEE TSE, Los Alamitos (1986)
Zee, K., Lam, P., Kuncak, V., Rinard, M.: Combining theorem proving with static analysis for data structure consistency. In: International Workshop on Software Verification and Validation (SVV 2004), Seattle (November 2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lam, P., Kuncak, V., Rinard, M. (2005). Generalized Typestate Checking for Data Structure Consistency. In: Cousot, R. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2005. Lecture Notes in Computer Science, vol 3385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30579-8_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-30579-8_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24297-0
Online ISBN: 978-3-540-30579-8
eBook Packages: Computer ScienceComputer Science (R0)