Abstract
We consider the problem of typestate verification for shallow programs; i.e., programs where pointers from program variables to heap-allocated objects are allowed, but where heap-allocated objects may not themselves contain pointers. We prove a number of results relating the complexity of verification to the nature of the finite state machine used to specify the property. Some properties are shown to be intractable, but others which appear to be quite similar admit polynomial-time verification algorithms. Our results serve to provide insight into the inherent complexity of important classes of verification problems. In addition, the program abstractions used for the polynomial-time verification algorithms may be of independent interest.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
K. Ashcraft and D. Engler. Using programmer-written compiler extensions to catch security holes. In Proc. IEEE Symp. on Security and Privacy, Oakland, CA, May 2002.
T. Ball, R. Majumdar, T. Millstein, and S. Rajamani. Automatic predicate abstraction of C programs. In Proc. ACM Conf. on Programming Language Design and Implementation, pages 203–213, June 2001.
T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN 2001: SPIN Workshop, LNCS 2057, pages 103–122, 2001.
E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV’00, July 2000.
E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In Proc. Intl. Conf. on Software Eng., pages 439–448, June 2000.
M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification in polynomial time. In Proc. ACM Conf. on Programming Language Design and Implementation, pages 57–68, Berlin, June 2002.
R. DeLine and M. Fähndrich. Enforcing high-level protocols in low-level software. In Proc. ACM Conf. on Programming Language Design and Implementation, pages 59–69, June 2001.
R. DeLine and M. Fähndrich. Adoption and focus: Practical linear types for imperative programming. In Proc. ACM Conf. on Programming Language Design and Implementation, pages 13–24, Berlin, June 2002.
E. W. Dijkstra. A Discipline of programing. Prentice-Hall, 1976.
J. Field, D. Goyal, G. Ramalingam, and E. Yahav. Shallow finite state verification. Technical Report RC22673, IBM T.J. Watson Research Center, Dec. 2002.
C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for java. In Proc. ACM Conf. on Programming Language Design and Implementation, pages 234–245, Berlin, June 2002.
J. S. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type qualifiers. In Proc. ACM Conf. on Programming Language Design and Implementation, pages 1–12, Berlin, June 2002.
R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. Journal of the ACM, 47(2):361–416, 2000.
S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In In Proceedings of the 9th Conference on Computer-Aided Verification (CAV’97), pages 72–83, Haifa, Israel, June 1997.
T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Symposium on Principles of Programming Languages, pages 58–70, 2002.
V. Kuncak, P. Lam, and M. Rinard. Role analysis. In Proc. ACM Symp. on Principles of Programming Languages, Portland, January 2002.
W. Landi and B. G. Ryder. Pointer-induced aliasing: A problem classification. In Proc. ACM Symp. on Principles of Programming Languages, pages 93–103, New York, NY, 1991. ACM Press.
W. Landi. Undecidability of static analysis. ACM Letters on Programming Languages and Systems, 1(4):323–337, December 1992.
R. Muth and S. Debray. On the complexity of flow-sensitive dataflow analyses. In Proc. ACM Symp. on Principles of Programming Languages, pages 67–80, New York, NY, 2000. ACM Press.
G. Naumovich, L. A. Clarke, L. J. Osterweil, and M. B. Dwyer. Verification of concurrent sofware with FLAVERS. In Proc. Intl. Conf. on Software Eng., pages 594–597, May 1997.
F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 2001.
G. Ramalingam, A. Warshavsky, J. Field, D. Goyal, and M. Sagiv. Deriving specialized program analyses for certifying component-client conformance. In Proc. ACM Conf. on Programming Language Design and Implementation, volume 37,5 of ACM SIGPLAN Notices, pages 83–94, New York, June 17–19 2002. ACM Press.
G. Ramalingam. The undecidability of aliasing. ACM Transactions on Programming Languages and Systems, 16(5):1467–1471, 1994.
T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Proc. ACM Symp. on Principles of Programming Languages, pages 49–61, 1995.
R. E. Strom and D. M. Yellin. Extending typestate checking using conditional liveness analysis. IEEE Trans. Software Eng., 19(5):478–485, May 1993.
R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Software Eng., 12(1):157–171, 1986.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Field, J., Goyal, D., Ramalingam, G., Yahav, E. (2003). Typestate Verification: Abstraction Techniques and Complexity Results. In: Cousot, R. (eds) Static Analysis. SAS 2003. Lecture Notes in Computer Science, vol 2694. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44898-5_25
Download citation
DOI: https://doi.org/10.1007/3-540-44898-5_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40325-8
Online ISBN: 978-3-540-44898-3
eBook Packages: Springer Book Archive