{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T22:33:09Z","timestamp":1693866789533},"reference-count":28,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2005,10,1]],"date-time":"2005-10-01T00:00:00Z","timestamp":1128124800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":2882,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2005,10]]},"DOI":"10.1016\/j.scico.2005.02.004","type":"journal-article","created":{"date-parts":[[2005,5,25]],"date-time":"2005-05-25T11:49:43Z","timestamp":1117021783000},"page":"57-82","source":"Crossref","is-referenced-by-count":10,"title":["Typestate verification: Abstraction techniques and complexity results"],"prefix":"10.1016","volume":"58","author":[{"given":"J.","family":"Field","sequence":"first","affiliation":[]},{"given":"D.","family":"Goyal","sequence":"additional","affiliation":[]},{"given":"G.","family":"Ramalingam","sequence":"additional","affiliation":[]},{"given":"E.","family":"Yahav","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.scico.2005.02.004_b1","doi-asserted-by":"crossref","unstructured":"K. Ashcraft, D. Engler, Using programmer-written compiler extensions to catch security holes, in: Proc. IEEE Symp. on Security and Privacy, May 2002, Oakland, CA","DOI":"10.1109\/SECPRI.2002.1004368"},{"key":"10.1016\/j.scico.2005.02.004_b2","doi-asserted-by":"crossref","unstructured":"T. Ball, R. Majumdar, T. Millstein, S. Rajamani, Automatic predicate abstraction of C programs, in: Proc. ACM Conf. on Programming Language Design and Implementation, June 2001, pp. 203\u2013213","DOI":"10.1145\/378795.378846"},{"key":"10.1016\/j.scico.2005.02.004_b3","series-title":"SPIN 2001: SPIN Workshop","first-page":"103","article-title":"Automatically validating temporal safety properties of interfaces","volume":"vol. 2057","author":"Ball","year":"2001"},{"key":"10.1016\/j.scico.2005.02.004_b4","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, Counterexample-guided abstraction refinement. in: CAV\u201900, July 2000","DOI":"10.1007\/10722167_15"},{"key":"10.1016\/j.scico.2005.02.004_b5","series-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"10.1016\/j.scico.2005.02.004_b6","doi-asserted-by":"crossref","unstructured":"J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, H. Zheng, Bandera: Extracting finite-state models from Java source code, in: Proc. Intl. Conf. on Software Eng., June 2000, pp. 439\u2013448","DOI":"10.1145\/337180.337234"},{"key":"10.1016\/j.scico.2005.02.004_b7","doi-asserted-by":"crossref","unstructured":"M. Das, S. Lerner, M. Seigle, ESP: Path-sensitive program verification in polynomial time, in: Proc. ACM Conf. on Programming Language Design and Implementation, June 2002, Berlin, 2002, pp. 57\u201368","DOI":"10.1145\/512537.512538"},{"key":"10.1016\/j.scico.2005.02.004_b8","doi-asserted-by":"crossref","unstructured":"R. DeLine, M. F\u00e4hndrich, Enforcing high-level protocols in low-level software, in: Proc. ACM Conf. on Programming Language Design and Implementation, June 2001, pp. 59\u201369","DOI":"10.1145\/378795.378811"},{"key":"10.1016\/j.scico.2005.02.004_b9","doi-asserted-by":"crossref","unstructured":"R. DeLine, M. F\u00e4hndrich, Adoption and focus: Practical linear types for imperative programming, in: Proc. ACM Conf. on Programming Language Design and Implementation, June 2002, Berlin, 2002, pp. 13\u201324","DOI":"10.1145\/512529.512532"},{"key":"10.1016\/j.scico.2005.02.004_b10","series-title":"A Discipline of Programing","author":"Dijkstra","year":"1976"},{"key":"10.1016\/j.scico.2005.02.004_b11","unstructured":"J. Field, D. Goyal, G. Ramalingam, E. Yahav, Shallow finite state verification, Technical Report RC22673, IBM T.J. Watson Research Center, December 2002"},{"key":"10.1016\/j.scico.2005.02.004_b12","doi-asserted-by":"crossref","unstructured":"C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J.B. Saxe, R. Stata, Extended static checking for java, in: Proc. ACM Conf. on Programming Language Design and Implementation, June 2002, Berlin, 2002, pp. 234\u2013245","DOI":"10.1145\/512557.512558"},{"key":"10.1016\/j.scico.2005.02.004_b13","doi-asserted-by":"crossref","unstructured":"J.S. Foster, T. Terauchi, A. Aiken, Flow-sensitive type qualifiers, in: Proc. ACM Conf. on Programming Language Design and Implementation, June 2002, Berlin, 2002, pp. 1\u201312","DOI":"10.1145\/512530.512531"},{"issue":"2","key":"10.1016\/j.scico.2005.02.004_b14","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1145\/333979.333989","article-title":"Making abstract interpretations complete","volume":"47","author":"Giacobazzi","year":"2000","journal-title":"J. ACM"},{"key":"10.1016\/j.scico.2005.02.004_b15","doi-asserted-by":"crossref","unstructured":"S. Graf, H. Saidi, Construction of abstract state graphs with PVS, in: Proceedings of the 9th Conference on Computer-Aided Verification, CAV\u201997, June 1997, Haifa, Israel, 1997, pp. 72\u201383","DOI":"10.1007\/3-540-63166-6_10"},{"key":"10.1016\/j.scico.2005.02.004_b16","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, R. Jhala, R. Majumdar, G. Sutre, Lazy abstraction, in: Symposium on Principles of Programming Languages, 2002, pp. 58\u201370","DOI":"10.1145\/503272.503279"},{"key":"10.1016\/j.scico.2005.02.004_b17","doi-asserted-by":"crossref","unstructured":"V. Kuncak, P. Lam, M. Rinard, Role analysis, in: Proc. ACM Symp. on Principles of Programming Languages, January 2002, Portland","DOI":"10.1145\/503272.503276"},{"issue":"4","key":"10.1016\/j.scico.2005.02.004_b18","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1145\/161494.161501","article-title":"Undecidability of static analysis","volume":"1","author":"Landi","year":"1992","journal-title":"ACM Lett. Program. Lang. Syst."},{"key":"10.1016\/j.scico.2005.02.004_b19","series-title":"Proc. ACM Symp. on Principles of Programming Languages","first-page":"93","article-title":"Pointer-induced aliasing: A problem classification","author":"Landi","year":"1991"},{"key":"10.1016\/j.scico.2005.02.004_b20","series-title":"Proc. ACM Symp. on Principles of Programming Languages","first-page":"67","article-title":"On the complexity of flow-sensitive dataflow analyses","author":"Muth","year":"2000"},{"key":"10.1016\/j.scico.2005.02.004_b21","doi-asserted-by":"crossref","unstructured":"G. Naumovich, L.A. Clarke, L.J. Osterweil, M.B. Dwyer, Verification of concurrent software with FLAVERS, in: Proc. Intl. Conf. on Software Eng., May 1997, pp. 594\u2013597","DOI":"10.1145\/253228.253489"},{"key":"10.1016\/j.scico.2005.02.004_b22","series-title":"Principles of Program Analysis","author":"Nielson","year":"2001"},{"issue":"5","key":"10.1016\/j.scico.2005.02.004_b23","doi-asserted-by":"crossref","first-page":"1467","DOI":"10.1145\/186025.186041","article-title":"The undecidability of aliasing","volume":"16","author":"Ramalingam","year":"1994","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.scico.2005.02.004_b24","series-title":"Proc. ACM Conf. on Programming Language Design and Implementation","first-page":"83","article-title":"Deriving specialized program analyses for certifying component-client conformance","volume":"vol. 37, 5","author":"Ramalingam","year":"2002"},{"key":"10.1016\/j.scico.2005.02.004_b25","doi-asserted-by":"crossref","unstructured":"T. Reps, S. Horwitz, M. Sagiv, Precise interprocedural dataflow analysis via graph reachability, in: Proc. ACM Symp. on Principles of Programming Languages, 1995, pp. 49\u201361","DOI":"10.1145\/199448.199462"},{"issue":"5","key":"10.1016\/j.scico.2005.02.004_b26","doi-asserted-by":"crossref","first-page":"478","DOI":"10.1109\/32.232013","article-title":"Extending typestate checking using conditional liveness analysis","volume":"19","author":"Strom","year":"1993","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"10.1016\/j.scico.2005.02.004_b27","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","article-title":"Typestate: A programming language concept for enhancing software reliability","volume":"12","author":"Strom","year":"1986","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/j.scico.2005.02.004_b28","series-title":"Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation","first-page":"25","article-title":"Verifying safety properties using separation and heterogeneous abstractions","author":"Yahav","year":"2004"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642305000444?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642305000444?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,7]],"date-time":"2020-04-07T11:55:19Z","timestamp":1586260519000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642305000444"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,10]]},"references-count":28,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2005,10]]}},"alternative-id":["S0167642305000444"],"URL":"https:\/\/doi.org\/10.1016\/j.scico.2005.02.004","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2005,10]]}}}