{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T05:24:25Z","timestamp":1736573065121,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540374060"},{"type":"electronic","value":"9783540374114"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11817963_49","type":"book-chapter","created":{"date-parts":[[2006,8,5]],"date-time":"2006-08-05T05:07:51Z","timestamp":1154754471000},"page":"547-561","source":"Crossref","is-referenced-by-count":19,"title":["Abstraction for Shape Analysis with Fast and Precise Transformers"],"prefix":"10.1007","author":[{"given":"Tal","family":"Lev-Ami","sequence":"first","affiliation":[]},{"given":"Neil","family":"Immerman","sequence":"additional","affiliation":[]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"49_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-30579-8_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis by predicate abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 164\u2013180. Springer, Heidelberg (2005)"},{"key":"49_CR2","doi-asserted-by":"crossref","unstructured":"Bingham, J., Rakamaric, Z.: A logic and decision procedure for predicate abstraction of heap-manipulating programs. Tech. Rep. TR-2005-19, Dept. of Comp. Sci., Univ. of BC, Canada (2005)","DOI":"10.1007\/11609773_14"},{"key":"49_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/3-540-44618-4_14","volume-title":"CONCUR 2000 - Concurrency Theory","author":"G. Bruns","year":"2000","unstructured":"Bruns, G., Godefroid, P.: Generalized model checking: Reasoning about partial state spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 168\u2013182. Springer, Heidelberg (2000)"},{"key":"49_CR4","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":"49_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"49_CR6","volume-title":"Symp. on Princ. of Prog. Lang.","author":"R. Ghiya","year":"1998","unstructured":"Ghiya, R., Hendren, L.: Putting pointer analysis to work. In: Symp. on Princ. of Prog. Lang., ACM Press, New York (1998)"},{"key":"49_CR7","doi-asserted-by":"crossref","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: CAV (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"49_CR8","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":"49_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-540-27813-9_22","volume-title":"Computer Aided Verification","author":"N. Immerman","year":"2004","unstructured":"Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: Verification via structure simulation. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 281\u2013294. Springer, Heidelberg (2004)"},{"key":"49_CR10","first-page":"102","volume-title":"Program Flow Analysis: Theory and Applications","author":"N.D. Jones","year":"1981","unstructured":"Jones, N.D., Muchnick, S.S.: Flow analysis and optimization of Lisp-like structures. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications, vol.\u00a04, pp. 102\u2013131. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"49_CR11","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA Version 1.4 User Manual. BRICS Notes Series NS-01-1, Dept. of Comp. Sci., Univ. of Aarhus (January 2001)"},{"key":"49_CR12","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: POPL (2006)","DOI":"10.1145\/1111037.1111048"},{"key":"49_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-31987-0_10","volume-title":"Programming Languages and Systems","author":"O. Lee","year":"2005","unstructured":"Lee, O., Yang, H., Yi, K.: Automatic verification of pointer programs using grammar-based shape analysis. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 124\u2013140. Springer, Heidelberg (2005)"},{"key":"49_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/11532231_8","volume-title":"Automated Deduction \u2013 CADE-20","author":"T. Lev-Ami","year":"2005","unstructured":"Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 99\u2013115. Springer, Heidelberg (2005)"},{"key":"49_CR15","unstructured":"Lev-Ami, T., Immerman, N., Sagiv, M.: Fast and precise abstraction for shape analysis. Technical Report TR-2006-01-001221, Tel-Aviv Univ.,(2006), Available at: http:\/\/www.cs.tau.ac.il\/~tla\/2006\/papers\/TR-2006-01-001221.pdf"},{"key":"49_CR16","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Static Analysis Symp., pp. 280\u2013301 (2000)","DOI":"10.1007\/978-3-540-45099-3_15"},{"key":"49_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-27864-1_20","volume-title":"Static Analysis","author":"R. Manevich","year":"2004","unstructured":"Manevich, R., Sagiv, M., Ramalingam, G., Field, J.: Partially disjunctive heap abstraction. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 265\u2013279. Springer, Heidelberg (2004)"},{"key":"49_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-540-30579-8_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Manevich","year":"2005","unstructured":"Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 181\u2013198. Springer, Heidelberg (2005)"},{"key":"49_CR19","doi-asserted-by":"crossref","unstructured":"Reps, T., Loginov, A., Sagiv, M.: Semantic minimization of 3-valued propositional formulae. In: LICS, pp. 40\u201354 (2002)","DOI":"10.1109\/LICS.2002.1029816"},{"key":"49_CR20","unstructured":"Cananda Sable Research\u00a0Group, McGill\u00a0University. Soot: a java optimization framework, Available at: http:\/\/www.sable.mcgill.ca\/soot\/"},{"key":"49_CR21","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. Trans. on Prog. Lang. and Syst. (2002)","DOI":"10.1145\/514188.514190"},{"key":"49_CR22","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":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11817963_49.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T09:58:34Z","timestamp":1736503114000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11817963_49"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540374060","9783540374114"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11817963_49","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}