skip to main content
research-article

Effective typestate verification in the presence of aliasing

Published: 05 May 2008 Publication History

Abstract

This article addresses the challenge of sound typestate verification, with acceptable precision, for real-world Java programs. We present a novel framework for verification of typestate properties, including several new techniques to precisely treat aliases without undue performance costs. In particular, we present a flow-sensitive, context-sensitive, integrated verifier that utilizes a parametric abstract domain combining typestate and aliasing information. To scale to real programs without compromising precision, we present a staged verification system in which faster verifiers run as early stages which reduce the workload for later, more precise, stages.
We have evaluated our framework on a number of real Java programs, checking correct API usage for various Java standard libraries. The results show that our approach scales to hundreds of thousands of lines of code, and verifies correctness for 93% of the potential points of failure.

References

[1]
Aiken, A., Foster, J. S., Kodumal, J., and Terauchi, T. 2003. Checking and inferring local non-aliasing. In Conference on Programming Language Design and Implementation (PLDI). SIGPLAN Not. 38, 5, 129--140.
[2]
Alur, R., Cerny, P., Madhusudan, P., and Nam, W. 2005. Synthesis of interface specifications for java classes. SIGPLAN Not. 40, 1, 98--109.
[3]
Andersen, L. O. 1994. Program analysis and specialization for the C programming language. Ph.D. thesis, DIKU, (DIKU report 94/19). University of Copenhagen.
[4]
Ashcraft, K. and Engler, D. 2002. Using programmer-written compiler extensions to catch security holes. In Proceedings of the IEEE Symposium on Security and Privacy. Oakland, CA.
[5]
Ball, T., Majumdar, R., Millstein, T., and Rajamani, S. 2001. Automatic predicate abstraction of C programs. In Proceedings of the ACM Conference on Programming Language Design and Implementation. 203--213.
[6]
Ball, T. and Rajamani, S. K. 2001. Automatically validating temporal safety properties of interfaces. In SPIN Workshop. Lecture Notes in Computer Science, vol. 2057. 103--122.
[7]
Ball, T. and Rajamani, S. K. 2002. The Slam project: debugging system software via static analysis. SIGPLAN Not. 37, 1, 1--3.
[8]
Chase, D. R., Wegman, M., and Zadeck, F. K. 1990. Analysis of pointers and structures. ACM SIGPLAN Not. 25, 6, 296--310. In Proceedings of the Conference on Programming Language Design and Implementation.
[9]
Choi, J.-D., Burke, M., and Carini, P. 1993. Efficient flow-sensitive interprocedural computation of pointer-induced aliases and side effects. In Proceedings of the ACM Symposium on Principles of Programming Languages 93. 232--245.
[10]
Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, Laubach, S., and Zheng, H. 2000. Bandera: Extracting finite-state models from Java source code. In Proceedings of the International Conference on Software Engineering 439--448.
[11]
Cousot, P. and Cousot, R. 1979. Systematic design of program analysis frameworks. In Proceedings of the ACM Symposium on Principles of Programming Languages. ACM Press, New York, NY, 269--282.
[12]
Crary, K., Walker, D., and Morrisett, G. 1999. Typed memory management in a calculus of capabilities. In Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of Programming Languages, (POPL'99), San Antonio, TX, ACM Press, New York, NY, 262--275.
[13]
Das, M. 2000. Unification-based point analysis with directional assignments. ACM SIGPLAN Not. 35, 5, 35--46.
[14]
Das, M., Lerner, S., and Seigle, M. 2002. ESP: path-sensitive program verification in polynomial time. ACM SIGPLAN Not. 37, 5, 57--68.
[15]
Degen, M., Thiemann, P., and Wehr, S. 2007. Tracking linear and affine resources with Java(X). In ECOOP Object-Oriented Programming. E. Ernst, Ed. Lecture Notes in Computer Science, vol. 4609. Springer-Verlag, 550--574.
[16]
DeLine, R. and Fähndrich, M. 2001. Enforcing high-level protocols in low-level software. In Proceedings of the ACM Conference on Programming Language Design and Implementation. 59--69.
[17]
DeLine, R. and Fähndrich, M. 2004. Typestates for objects. In Proceedings of the 18th European Conference on Object-Oriented Programming (ECOOP). Lecture Notes in Computer Science, Vol. 3086.
[18]
Dor, N., Adams, S., Das, M., and Yang, Z. 2004. Software validation via scalable path-sensitive value flow analysis. In Proceedings of the International Symposium on Software Testing and Analysis. 12--22.
[19]
Dwyer, M. B. and Clarke, L. A. 1994. Data flow analysis for verifying properties of concurrent programs. In Proceedings of the 2nd ACM SIGSOFT Symposium on Foundations of Software Engineering. New Orleans, LA, 62--75.
[20]
Emami, M., Ghiya, R., and Hendren, L. J. 1994. Context-sensitive interprocedural points-to analysis in the presence of function pointers. ACM SIGPLAN Not. 29, 6, 242--256. In Proceedings of the Conference on Programming Language Design and Implementation.
[21]
Fähndrich, M. and DeLine, R. 2002. Adoption and focus: practical linear types for imperative programming. ACM SIGPLAN Not. 37, 5, 13--24. In Proceedings of the Conference on Programming Language Design and Implementation.
[22]
Field, J., Goyal, D., Ramalingam, G., and Yahav, E. 2003. Typestate verification: Abstraction techniques and complexity results. In Proceedings of the Static Analysis Symposium (SAS'03). Lecture Notes in Computer Science, vol. 2694. Springer, 439--462.
[23]
Fink, S., Dolby, J., and Colby, L. 2004. Semi-automatic J2EE transaction configuration. Tech. rep. RC23326, IBM.
[24]
Flanagan, C., Leino, K. R. M., Lillibridge, M., Nelson, G., Saxe, J. B., and Stata, R. 2002. Extended static checking for java. In Proceedings of the ACM Conference on Programming Language Design and Implementation. Berlin Germany, 234--245.
[25]
Foster, J. S., Terauchi, T., and Aiken, A. 2002. Flow-sensitive type qualifiers. In Proceedings of the ACM Conference on Programming Language Design and Implementation. Berlin Germany, 1--12.
[26]
Grove, D. and Chambers, C. 2001. A framework for call graph construction algorithms. Trans. Program. Langu. Syst. 23, 6, 685--746.
[27]
Gupta, R. 1993. Optimizing array bound checks using flow analysis. ACM Lett. Program. Lang. Syst. 2, 1-4, 135--150.
[28]
Guyer, S. and Lin, C. 2003. Client-driven pointer analysis. In Proceedings of the SAS'03. Lecture Notes in Computer Science, vol. 2694. 214--236.
[29]
Hackett, B. and Rugina, R. 2005. Region-based shape analysis with tracked locations. In Proceedings of the ACM Symposium on Principles of Programming Languages. J. Palsberg and M. Abadi, Eds. ACM, 310--323.
[30]
Hasti, R. and Horwitz, S. 1998. Using static single assignment form to improve flow-insensitive pointer analysis. ACM SIGPLAN Not. 33, 5, 97--105.
[31]
Heintze, N. and Tardieu, O. 2001. Ultra-fast aliasing analysis using CLA: A million lines of C code in a second. ACM SIGPLAN Not. 36, 5, 254--263.
[32]
Henzinger, T. A., Jhala, R., Majumdar, R., and Sutre, G. 2002. Lazy abstraction. In Proceedings of the Symposium on Principles of Programming Languages. 58--70.
[33]
Landi, W. and Ryder, B. G. 1992. A safe approximate algorithm for interprocedural aliasing. ACM SIGPLAN Not. 27, 7, 235--248.
[34]
Lhoták, O. and Hendren, L. 2003. Scaling Java points-to analysis using SPARK. In Proceedings of the 12th International Conference on Compiler Construction (CC). Lecture Notes in Computer Science, vol. 2622. 153--169.
[35]
Livshits, B., Whaley, J., and Lam, M. S. 2005. Reflection analysis for java. In Proceedings of Asian Symposium Programming Languages and Systems: 3rd (APLAS).
[36]
Milanova, A., Rountev, A., and Ryder, B. G. 2005. Parameterized object sensitivity for points-to analysis for java. ACM Trans. Softw. Eng. Method. 14, 1, 1--41.
[37]
Naumovich, G., Avrunin, G. S., and Clarke, L. A. 1999. Data flow analysis for checking properties of concurrent java programs. In Proceedings of the International Conference on Software Engineering. Los Angeles, CA 399--410.
[38]
Plevyak, J. and Chien, A. A. 1994. Precise concrete type inference for object-oriented languages. In ACM SIGPLAN Not. 29, 10, 324.
[39]
Ramalingam, G. 2002. On sparse evaluation representations. Theor. Comput. Sci. 277, 1-2, 119--147.
[40]
Ramalingam, G., Warshavsky, A., Field, J., Goyal, D., and Sagiv, M. 2002. Deriving specialized program analyses for certifying component-client conformance. In Proceedings of the ACM Conference. ACM SIGPLAN Not., 37, 5. 83--94.
[41]
Reps, T., Horwitz, S., and Sagiv, M. 1995. Precise interprocedural dataflow analysis via graph reachability. In Proceedings of the ACM Symposium on Principles of Programming Languages. 49--61.
[42]
Sagiv, M., Reps, T., and Wilhelm, R. 2002. Parametric shape analysis via 3-valued logic. Trans. Program. Lang. Syst. 24, 3, 217--298.
[43]
Sharir, M. and Pneuli, A. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications.
[44]
Shoham, S., Yahav, E., Fink, S., and Pistoia, M. 2007. Static specification mining using automata-based abstractions. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA).
[45]
Steensgaard, B. 1996. Points-to analysis in almost linear time. In Conference Record of 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages: 32--41.
[46]
Strom, R. E. and Yemini, S. 1986. Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng. 12, 1, 157--171.
[47]
Whaley, J., Martin, M., and Lam, M. 2002. Automatic extraction of object-oriented component interfaces. In Proceedings of the International Symposium on Software Testing and Analysis.
[48]
Wilson, R. P. and Lam, M. S. 1995. Efficient context-sensitive pointer analysis for C programs. ACM SIGPLAN Not. 30, 6, 1--12.
[49]
Yahav, E. and Ramalingam, G. 2004. Verifying safety properties using separation and heterogeneous abstractions. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, 25--34.
[50]
Yorsh, G., Yahav, E., and Chandra, S. 2007. Symbolic summarization with applications to typestate verification. Tech. rep., Tel Aviv University (www.cs.tau.ac.il/~gretay).

Cited By

View all
  • (2025)Stack Filtering: Elevating Precision and Efficiency in Rust Pointer AnalysisProceedings of the 23rd ACM/IEEE International Symposium on Code Generation and Optimization10.1145/3696443.3708921(331-346)Online publication date: 1-Mar-2025
  • (2024)Balancing analysis time and bug detectionProceedings of the 2024 USENIX Conference on Usenix Annual Technical Conference10.5555/3691992.3692023(493-508)Online publication date: 10-Jul-2024
  • (2024)rOOM: A Rust-Based Linux Out of Memory Kernel ComponentIEICE Transactions on Information and Systems10.1587/transinf.2023MPP0001E107.D:3(245-256)Online publication date: 1-Mar-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Software Engineering and Methodology
ACM Transactions on Software Engineering and Methodology  Volume 17, Issue 2
April 2008
207 pages
ISSN:1049-331X
EISSN:1557-7392
DOI:10.1145/1348250
Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 May 2008
Accepted: 01 July 2007
Received: 01 April 2007
Published in TOSEM Volume 17, Issue 2

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Alias analysis
  2. program verification
  3. typestate

Qualifiers

  • Research-article
  • Research
  • Refereed

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)62
  • Downloads (Last 6 weeks)5
Reflects downloads up to 22 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2025)Stack Filtering: Elevating Precision and Efficiency in Rust Pointer AnalysisProceedings of the 23rd ACM/IEEE International Symposium on Code Generation and Optimization10.1145/3696443.3708921(331-346)Online publication date: 1-Mar-2025
  • (2024)Balancing analysis time and bug detectionProceedings of the 2024 USENIX Conference on Usenix Annual Technical Conference10.5555/3691992.3692023(493-508)Online publication date: 10-Jul-2024
  • (2024)rOOM: A Rust-Based Linux Out of Memory Kernel ComponentIEICE Transactions on Information and Systems10.1587/transinf.2023MPP0001E107.D:3(245-256)Online publication date: 1-Mar-2024
  • (2024)SPATA: Effective OS Bug Detection with Summary-Based, Alias-Aware, and Path-Sensitive Typestate AnalysisACM Transactions on Computer Systems10.1145/369525042:3-4(1-40)Online publication date: 6-Sep-2024
  • (2024)To Tag, or Not to Tag: Translating C's Unions to Rust's Tagged UnionsProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3694985(40-52)Online publication date: 27-Oct-2024
  • (2024)Scaling Abstraction Refinement for Program Analyses in Datalog using Graph Neural NetworksProceedings of the ACM on Programming Languages10.1145/36897658:OOPSLA2(1532-1560)Online publication date: 8-Oct-2024
  • (2024)Law and Order for Typestate with BorrowingProceedings of the ACM on Programming Languages10.1145/36897638:OOPSLA2(1475-1503)Online publication date: 8-Oct-2024
  • (2024)Symbol-Specific Sparsification of Interprocedural Distributive Environment ProblemsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639092(1-12)Online publication date: 20-May-2024
  • (2023)Tai-e: A Developer-Friendly Static Analysis Framework for Java by Harnessing the Good Designs of ClassicsProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598120(1093-1105)Online publication date: 12-Jul-2023
  • (2023)Context Sensitivity without Contexts: A Cut-Shortcut Approach to Fast and Precise Pointer AnalysisProceedings of the ACM on Programming Languages10.1145/35912427:PLDI(539-564)Online publication date: 6-Jun-2023
  • Show More Cited By

View Options

Login options

Full Access

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media