{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:33:47Z","timestamp":1761597227510},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223429"},{"type":"electronic","value":"9783540278139"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27813-9_22","type":"book-chapter","created":{"date-parts":[[2010,9,14]],"date-time":"2010-09-14T00:57:57Z","timestamp":1284425877000},"page":"281-294","source":"Crossref","is-referenced-by-count":16,"title":["Verification via Structure Simulation"],"prefix":"10.1007","author":[{"given":"Niel","family":"Immerman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Rabinovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas W.","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Great","family":"Yorsh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Benedikt, M., Reps, T., Sagiv, M.: A decidable logic for describing linked data structures. In: European Symp. On Programming, pp. 2\u201319 (March 1999)","DOI":"10.1007\/3-540-49099-X_2"},{"key":"22_CR2","first-page":"269","volume-title":"Symp. on Princ. of Prog. Lang.","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Symp. on Princ. of Prog. Lang., pp. 269\u2013282. ACM Press, New York (1979)"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Elgaard, J., M\u00f8ller, A., Schwartzbach, M.I.: Compile-time debugging of C programs working on trees. In: European Symp. On Programming, pp. 119\u2013134 (2000)","DOI":"10.1007\/3-540-46425-5_8"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Hendren, L.: Parallelizing Programs with Recursive Data Structures. PhD thesis, Cornell Univ., Ithaca, NY (January 1990)","DOI":"10.1145\/318789.318812"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.G. Henriksen","year":"1995","unstructured":"Henriksen, J.G., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019, Springer, Heidelberg (1995)"},{"key":"22_CR6","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Proof of correctness of data representations. Acta Inf.\u00a01, 271\u2013281 (1972)","journal-title":"Acta Inf."},{"issue":"2","key":"22_CR7","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00976239","volume":"4","author":"C.A.R. Hoare","year":"1975","unstructured":"Hoare, C.A.R.: Recursive data structures. Int. J. of Comp. and Inf. Sci.\u00a04(2), 105\u2013132 (1975)","journal-title":"Int. J. of Comp. and Inf. Sci."},{"key":"22_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0539-5","volume-title":"Descriptive Complexity","author":"N. Immerman","year":"1999","unstructured":"Immerman, N.: Descriptive Complexity. Springer, Heidelberg (1999)"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The boundery between decidability and undecidability of transitive closure logics (2004) (submitted for publication)","DOI":"10.1007\/978-3-540-30124-0_15"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: SIGPLAN Conf. on Prog. Lang. Design and Impl., pp. 221\u2013231 (2001)","DOI":"10.1145\/381694.378851"},{"key":"22_CR11","first-page":"1","volume":"141","author":"M. Rabin","year":"1969","unstructured":"Rabin, M.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc.\u00a0141, 1\u201335 (1969)","journal-title":"Trans. Amer. Math. Soc."},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"issue":"1","key":"22_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/271510.271517","volume":"20","author":"M. Sagiv","year":"1998","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. Trans. on Prog. Lang. and Syst.\u00a020(1), 1\u201350 (1998)","journal-title":"Trans. on Prog. Lang. and Syst."},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-540-24730-2_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Yorsh","year":"2004","unstructured":"Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 530\u2013545. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27813-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T18:17:59Z","timestamp":1558289879000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27813-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223429","9783540278139"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27813-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}