{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T13:32:38Z","timestamp":1726407158374},"publisher-location":"Berlin, Heidelberg","reference-count":36,"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_24","type":"book-chapter","created":{"date-parts":[[2007,11,11]],"date-time":"2007-11-11T03:21:25Z","timestamp":1194751285000},"page":"418-438","source":"Crossref","is-referenced-by-count":8,"title":["Existential Heap Abstraction Entailment Is Undecidable"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,5,13]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Michael Benedikt, Thomas Reps, and Mooly Sagiv. A decidable logic for linked data structures. In Proc. 8th European Symposium on Programming, 1999.","DOI":"10.1007\/3-540-49099-X_2"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"Egon B\u00f6rger, Erich Gr\u00e4edel, and Yuri Gurevich. The Classical Decision Problem. Springer-Verlag, 1997.","DOI":"10.1007\/978-3-642-59207-2"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Cristiano Calcagno, Luca Cardelli, and Andrew D. Gordon. Deciding validity in a spatial logic for trees. Submitted, September 2002.","DOI":"10.1145\/604174.604183"},{"issue":"8","key":"24_CR4","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1007\/s00236-002-0081-8","volume":"38","author":"V. T. Chakaravarthy","year":"2002","unstructured":"Venkatesan T. Chakaravarthy and Susan B. Horwitz. On the non-approximability of points-to analysis. Acta Informatica, 38(8):587\u2013598, June 2002.","journal-title":"Acta Informatica"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"David R. Chase, Mark Wegman, and F. Kenneth Zadeck. Analysis of pointers and structures. In Proc. ACM PLDI, 1990.","DOI":"10.1145\/93542.93585"},{"key":"24_CR6","unstructured":"H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Available on: http:\/\/www.grappa.univ-lille3.fr\/tata, 1997. release 1 October 2002."},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Bruno Courcelle. The expression of graph properties and graph transformations in monadic second-order logic. In Handbook of graph grammars and computing by graph transformations, Vol. 1: Foundations, chapter 5. World Scientific, 1997.","DOI":"10.1142\/9789812384720_0005"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Manuvir Das, Sorin Lerner, and Mark Seigle. ESP: Path-sensitive program verification in polynomial time. In Proc. ACM PLDI, 2002.","DOI":"10.1145\/512529.512538"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Robert DeLine and Manuel F\u00e4hndrich. Enforcing high-level protocols in low-level software. In Proc. ACM PLDI, 2001.","DOI":"10.1145\/378795.378811"},{"key":"24_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1007\/3-540-45337-7_8","volume-title":"Proc. 15th European Conference on Object-Oriented Programming","author":"S. Drossopoulou","year":"2001","unstructured":"S. Drossopoulou, F. Damiani, M. Dezani-Ciancaglini, and P. Giannini. Fickle: Dynamic object re-classification. In Proc. 15th European Conference on Object-Oriented Programming, LNCS 2072, pages 130\u2013149. Springer, 2001."},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Dawson Engler, Benjamin Chelf, Andy Chou, and Seth Hallem. Checking system rules using systemspecific, programmer-written compiler extensions. In Proc. 4th USENIX Symposium on Operating Systems Design and Implementation, 2000.","DOI":"10.21236\/ADA419626"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Ronald Fagin, Larry J. Stockmeyer, and Moshe Y. Vardi. On monadic NP vs monadic co-NP. Information and Computation, 120(1), 1995.","DOI":"10.1006\/inco.1995.1100"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Cormac Flanagan, K. Rustan M. Leino, Mark Lilibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended Static Checking for Java. In Proc. ACM PLDI, 2002.","DOI":"10.1145\/512529.512558"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. Flow-sensitive type qualifiers. In Proc. ACM PLDI, 2002.","DOI":"10.1145\/512529.512531"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Pascal Fradet and Daniel Le Metayer. Shape types. In Proc. 24th ACM POPL, 1997.","DOI":"10.1145\/263699.263706"},{"key":"24_CR16","unstructured":"Rakesh Ghiya and Laurie Hendren. Is it a tree, a DAG, or a cyclic graph? In Proc. 23rd ACM POPL, 1996."},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Dora Giammarresi and Antonio Restivo. Two-dimensional languages. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages Vol.3: Beyond Words. Springer-Verlag, 1997.","DOI":"10.1007\/978-3-642-59126-6_4"},{"key":"24_CR18","unstructured":"Wilfrid Hodges. Model Theory, volume 42 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1993."},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Neil Immerman. Descriptive Complexity. Springer-Verlag, 1998.","DOI":"10.1007\/978-1-4612-0539-5"},{"key":"24_CR20","unstructured":"Daniel Jackson. Alloy: A lightweight object modelling notation. Technical Report 797, MIT Laboratory for Computer Science, 2000."},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Viktor Kuncak, Patrick Lam, and Martin Rinard. Role analysis. In Proc. 29th ACM POPL, 2002.","DOI":"10.1145\/503272.503276"},{"key":"24_CR22","unstructured":"Viktor Kuncak and Martin Rinard. Typestate checking and regular graph constraints. Technical Report 863, MIT Laboratory for Computer Science, 2002. http:\/\/www.mit.edu\/~vkuncak\/papers\/index.html."},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"James R. Larus and Paul N. Hilfinger. Detecting conflicts between structure accesses. In Proc. ACM PLDI, Atlanta, GA, June 1988.","DOI":"10.1145\/53990.53993"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"Anders M\u00f8ller and Michael I. Schwartzbach. The Pointer Assertion Logic Engine. In Proc. ACM PLDI, 2001.","DOI":"10.1145\/378795.378851"},{"key":"24_CR25","unstructured":"Greg Nelson. Techniques for program verification. Technical report, XEROX Palo Alto Research Center, 1981."},{"key":"24_CR26","doi-asserted-by":"crossref","unstructured":"Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis. Springer-Verlag, 1999.","DOI":"10.1007\/978-3-662-03811-6"},{"issue":"5","key":"24_CR27","doi-asserted-by":"publisher","first-page":"1467","DOI":"10.1145\/186025.186041","volume":"16","author":"G. Ramalingam","year":"1994","unstructured":"Ganesan Ramalingam. The undecidability of aliasing. ACM Transactions on Programming Languages and Systems (TOPLAS), 16(5):1467\u20131471, 1994.","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"24_CR28","first-page":"25","volume":"89","author":"H. G. Rice","year":"1953","unstructured":"H. G. Rice. Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society, 89:25\u201329, 1953.","journal-title":"Transactions of the American Mathematical Society"},{"key":"24_CR29","doi-asserted-by":"crossref","unstructured":"Neil Robertson and Paul D. Seymour. Graph minors: A survey. In Ian Anderson, editor, Surveys in Combinatorics Papers for the London Math. Soc. Lecture Note Series, 1985.","DOI":"10.1017\/CBO9781107325678.009"},{"issue":"1","key":"24_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/271510.271517","volume":"20","author":"M. Sagiv","year":"1998","unstructured":"Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Solving shape-analysis problems in languages with destructive updating. ACM TOPLAS, 20(1):1\u201350, 1998.","journal-title":"ACM TOPLAS"},{"issue":"3","key":"24_CR31","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric shape analysis via 3-valued logic. ACM TOPLAS, 24(3):217\u2013298, 2002.","journal-title":"ACM TOPLAS"},{"key":"24_CR32","unstructured":"Michael Sipser. Introduction to the Theory of Computation. PWS Publishing Company, 1997."},{"key":"24_CR33","doi-asserted-by":"crossref","unstructured":"F. Smith, D. Walker, and G. Morrisett. Alias types. In Proc. 9th European Symposium on Programming, Berlin, Germany, March 2000.","DOI":"10.1007\/3-540-46425-5_24"},{"key":"24_CR34","doi-asserted-by":"crossref","unstructured":"Robert E. Strom and Shaula Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, January 1986.","DOI":"10.1109\/TSE.1986.6312929"},{"key":"24_CR35","doi-asserted-by":"crossref","unstructured":"Wolfgang Thomas. Languages, automata, and logic. In Handbook of Formal Languages Vol.3: Beyond Words. Springer-Verlag, 1997.","DOI":"10.1007\/978-3-642-59126-6_7"},{"key":"24_CR36","doi-asserted-by":"crossref","unstructured":"David Walker and Greg Morrisett. Alias types for recursive data structures. In Workshop on Types in Compilation, 2000.","DOI":"10.1007\/3-540-45332-6_7"}],"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_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T09:20:55Z","timestamp":1556961655000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44898-5_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540403258","9783540448983"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-44898-5_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}