{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:08:26Z","timestamp":1725494906115},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540403258"},{"type":"electronic","value":"9783540448983"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44898-5_25","type":"book-chapter","created":{"date-parts":[[2007,11,11]],"date-time":"2007-11-11T03:21:25Z","timestamp":1194751285000},"page":"439-462","source":"Crossref","is-referenced-by-count":10,"title":["Typestate Verification: Abstraction Techniques and Complexity Results"],"prefix":"10.1007","author":[{"given":"John","family":"Field","sequence":"first","affiliation":[]},{"given":"Deepak","family":"Goyal","sequence":"additional","affiliation":[]},{"given":"G.","family":"Ramalingam","sequence":"additional","affiliation":[]},{"given":"Eran","family":"Yahav","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,5,13]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1109\/SECPRI.2002.1004368"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"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\u2013213, June 2001.","DOI":"10.1145\/378795.378846"},{"key":"25_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/3-540-45420-9","volume-title":"SPIN 2001: SPIN Workshop","author":"T. Ball","year":"2001","unstructured":"T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN 2001: SPIN Workshop, LNCS 2057, pages 103\u2013122, 2001."},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV\u201900, July 2000.","DOI":"10.1007\/10722167_15"},{"key":"25_CR5","unstructured":"E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"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\u2013448, June 2000.","DOI":"10.1145\/337180.337234"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"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\u201368, Berlin, June 2002.","DOI":"10.1145\/512529.512538"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"R. DeLine and M. F\u00e4hndrich. Enforcing high-level protocols in low-level software. In Proc. ACM Conf. on Programming Language Design and Implementation, pages 59\u201369, June 2001.","DOI":"10.1145\/378795.378811"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"R. DeLine and M. F\u00e4hndrich. Adoption and focus: Practical linear types for imperative programming. In Proc. ACM Conf. on Programming Language Design and Implementation, pages 13\u201324, Berlin, June 2002.","DOI":"10.1145\/543552.512532"},{"key":"25_CR10","unstructured":"E. W. Dijkstra. A Discipline of programing. Prentice-Hall, 1976."},{"key":"25_CR11","unstructured":"J. Field, D. Goyal, G. Ramalingam, and E. Yahav. Shallow finite state verification. Technical Report RC22673, IBM T.J. Watson Research Center, Dec. 2002."},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"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\u2013245, Berlin, June 2002.","DOI":"10.1145\/512529.512558"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"J. S. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type qualifiers. In Proc. ACM Conf. on Programming Language Design and Implementation, pages 1\u201312, Berlin, June 2002.","DOI":"10.1145\/512529.512531"},{"issue":"2","key":"25_CR14","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1145\/333979.333989","volume":"47","author":"R. Giacobazzi","year":"2000","unstructured":"R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. Journal of the ACM, 47(2):361\u2013416, 2000.","journal-title":"Journal of the ACM"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In In Proceedings of the 9th Conference on Computer-Aided Verification (CAV\u201997), pages 72\u201383, Haifa, Israel, June 1997.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Symposium on Principles of Programming Languages, pages 58\u201370, 2002.","DOI":"10.1145\/503272.503279"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"V. Kuncak, P. Lam, and M. Rinard. Role analysis. In Proc. ACM Symp. on Principles of Programming Languages, Portland, January 2002.","DOI":"10.1145\/503272.503276"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"W. Landi and B. G. Ryder. Pointer-induced aliasing: A problem classification. In Proc. ACM Symp. on Principles of Programming Languages, pages 93\u2013103, New York, NY, 1991. ACM Press.","DOI":"10.1145\/99583.99599"},{"issue":"4","key":"25_CR19","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/161494.161501","volume":"1","author":"W. Landi","year":"1992","unstructured":"W. Landi. Undecidability of static analysis. ACM Letters on Programming Languages and Systems, 1(4):323\u2013337, December 1992.","journal-title":"ACM Letters on Programming Languages and Systems"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"R. Muth and S. Debray. On the complexity of flow-sensitive dataflow analyses. In Proc. ACM Symp. on Principles of Programming Languages, pages 67\u201380, New York, NY, 2000. ACM Press.","DOI":"10.1145\/325694.325704"},{"key":"25_CR21","doi-asserted-by":"crossref","unstructured":"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\u2013597, May 1997.","DOI":"10.1145\/253228.253489"},{"key":"25_CR22","unstructured":"F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 2001."},{"issue":"5","key":"25_CR23","first-page":"83","volume":"37","author":"G. Ramalingam","year":"2002","unstructured":"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\u201394, New York, June 17\u201319 2002. ACM Press.","journal-title":"Proc. ACM Conf. on Programming Language Design and Implementation"},{"issue":"5","key":"25_CR24","doi-asserted-by":"publisher","first-page":"1467","DOI":"10.1145\/186025.186041","volume":"16","author":"G. Ramalingam","year":"1994","unstructured":"G. Ramalingam. The undecidability of aliasing. ACM Transactions on Programming Languages and Systems, 16(5):1467\u20131471, 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"25_CR25","doi-asserted-by":"crossref","unstructured":"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\u201361, 1995.","DOI":"10.1145\/199448.199462"},{"issue":"5","key":"25_CR26","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1109\/32.232013","volume":"19","author":"R. E. Strom","year":"1993","unstructured":"R. E. Strom and D. M. Yellin. Extending typestate checking using conditional liveness analysis. IEEE Trans. Software Eng., 19(5):478\u2013485, May 1993.","journal-title":"IEEE Trans. Software Eng."},{"issue":"1","key":"25_CR27","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","volume":"12","author":"R. E. Strom","year":"1986","unstructured":"R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Software Eng., 12(1):157\u2013171, 1986.","journal-title":"IEEE Trans. Software Eng."}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44898-5_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T09:21:06Z","timestamp":1556961666000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44898-5_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540403258","9783540448983"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-44898-5_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}