{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:34:03Z","timestamp":1761597243825},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540242970"},{"type":"electronic","value":"9783540305798"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30579-8_12","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T16:45:34Z","timestamp":1292863534000},"page":"164-180","source":"Crossref","is-referenced-by-count":57,"title":["Shape Analysis by Predicate Abstraction"],"prefix":"10.1007","author":[{"given":"Ittai","family":"Balaban","sequence":"first","affiliation":[]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[]},{"given":"Lenore D.","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/3-540-61474-5_68","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"1996","unstructured":"Pnueli, A., Shahar, E.: A platform combining deductive with algorithmic verification. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, p. 184. Springer, Heidelberg (1996)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 221\u2013234. Springer, Heidelberg (2001)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Tools and Algorithms for Construction and Analysis of Systems, pp. 158\u2013172 (2002)","DOI":"10.1007\/3-540-46002-0_12"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45139-0_7","volume-title":"Model Checking Software","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, p. 103. Springer, Heidelberg (2001)"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Benedikt, M., Reps, T.W., Sagiv, S.: A decidable logic for describing linked data structures. In: European Symposium on Programming, pp. 2\u201319 (1999)","DOI":"10.1007\/3-540-49099-X_2"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/3-540-36384-X_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Dams","year":"2002","unstructured":"Dams, D., Namjoshi, K.S.: Shape analysis through predicate abstraction and model checking. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 310\u2013324. Springer, Heidelberg (2002)"},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1109\/LICS.2001.932482","volume-title":"Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science","author":"S. Das","year":"2001","unstructured":"Das, S., Dill, D.L.: Successive approximation of abstract transition relations. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p. 51. IEEE Computer Society, Los Alamitos (2001)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer Aided Verification","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 160\u2013171. Springer, Heidelberg (1999)"},{"key":"12_CR10","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1145\/503272.503291","volume-title":"Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 191\u2013202. ACM Press, New York (2002)"},{"key":"12_CR11","first-page":"102","volume-title":"Program Flow Analysis: Theory and Applications, ch. 4","author":"N. Jones","year":"1981","unstructured":"Jones, N., Muchnick, S.: Flow analysis and optimization of Lisp-like structures. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Applications, ch. 4, pp. 102\u2013131. Prentice-Hall, Englewood Cliffs (1981)"},{"issue":"1","key":"12_CR12","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation\u00a0163(1), 203\u2013243 (2000)","journal-title":"Information and Computation"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Nelson, G.: Verifying Reachability Invariants of Linked Structures. In: Proc. 10th ACM Symp. Princ. of Prog. Lang., pp. 38\u201347 (1983)","DOI":"10.1145\/567067.567073"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"issue":"3","key":"12_CR16","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst.\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30579-8_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:31:22Z","timestamp":1620012682000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30579-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242970","9783540305798"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30579-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}