{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:54:22Z","timestamp":1754484862709,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540003489"},{"type":"electronic","value":"9783540363842"}],"license":[{"start":{"date-parts":[[2002,12,16]],"date-time":"2002-12-16T00:00:00Z","timestamp":1039996800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36384-x_25","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T14:21:13Z","timestamp":1196346073000},"page":"310-323","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Shape Analysis through Predicate Abstraction and Model Checking"],"prefix":"10.1007","author":[{"given":"Dennis","family":"Dams","sequence":"first","affiliation":[]},{"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,12,16]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"T. Ball, R. Majumdar, T.D. Millstein, and S.K. Rajamani. Automatic predicate abstraction of C programs. In PLDI, 2001.","DOI":"10.1145\/378795.378846"},{"key":"25_CR2","series-title":"Lect Notes Comput Sci","volume-title":"TACAS","author":"T. Ball","year":"2002","unstructured":"T. Ball, A. Podelski, and S. Rajamani. Relative completeness of abstraction refinement for software model checking. In TACAS, volume 2280 of LNCS, 2002."},{"key":"25_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45420-9","volume-title":"CAV","author":"T. Ball","year":"2001","unstructured":"T. Ball and S. Rajamani. The SLAM toolkit. In CAV, volume 2102 of LNCS, 2001."},{"key":"25_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-49099-X_2","volume-title":"ESOP","author":"M. Benedikt","year":"1999","unstructured":"M. Benedikt, T. Reps, and M. Sagiv. A decidable logic for describing linked data structures. In ESOP, volume 1576 of LNCS, pages 2\u201319, 1999."},{"key":"25_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/10722010_8","volume-title":"Mathematics of Program Construction","author":"R. Bornat","year":"2000","unstructured":"R. Bornat. Proving pointer programs in Hoare logic. In Mathematics of Program Construction, volume 1837 of LNCS, pages 102\u2013126, 2000."},{"key":"25_CR6","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"E.M. Clarke","year":"2000","unstructured":"E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV, volume 1855 of LNCS, 2000."},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 238\u2013252, 1977.","DOI":"10.1145\/512950.512973"},{"key":"25_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Programming Language Implementation and Logic Programming","author":"P. Cousot","year":"1992","unstructured":"Patrick Cousot and Radhia Cousot. Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, Programming Language Implementation and Logic Programming, volume 631 of LNCS, pages 269\u2013295, 1992."},{"key":"25_CR9","unstructured":"S. Das and D. Dill. Successive approximation of abstract transition relations. In LICS, 2001."},{"key":"25_CR10","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"S. Das","year":"1999","unstructured":"S. Das, D. Dill, and S. Park. Experience with predicate abstraction. In CAV, volume 1633 of LNCS, 1999."},{"key":"25_CR11","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. A computing procedure for quantification theory. J. Assoc. Computing Machinery, 7:201\u2013215, 1960.","journal-title":"J. Assoc. Computing Machinery"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"E.W. Dijkstra. Guarded commands, nondeterminacy, and formal derivation of programs. C.ACM, 18, 1975.","DOI":"10.1145\/800027.808417"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In POPL, 2002.","DOI":"10.1145\/503272.503291"},{"key":"25_CR14","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"S. Graf","year":"1997","unstructured":"S. Graf and H. Sa\u00efdi. Construction of abstract state graphs with PVS. In CAV, volume 1254 of LNCS, 1997."},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"D. Gries. The Science Of Programming. Springer-Verlag, 1981.","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"25_CR16","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"R.H. Hardin","year":"1996","unstructured":"R.H. Hardin, Z. Har\u2019el, and R.P. Kurshan. COSPAN. In CAV, volume 1102 of LNCS, 1996."},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL, 2002.","DOI":"10.1145\/503272.503279"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"G. Holzmann. The SPIN model checker. IEEE Transactions on Software Engineering, 23(5), May 1997.","DOI":"10.1109\/32.588521"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"J.L. Jensen, M.E. Jorgensen, N. Klarlund, and M.I. Schwartzbach. Automatic verification of pointer programs using monadic second-order logic. In SIGPLAN Conference on Programming Language Design and Implementation, pages 226\u2013236, 1997.","DOI":"10.1145\/258916.258936"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"M. Kaufmann, P. Manolios, and J.S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"25_CR21","doi-asserted-by":"crossref","unstructured":"N. Klarlund and M.I. Schwartzbach. Graphs and decidable transductions based on edge constraints (extended abstract). In Colloquium on Trees in Algebra and Programming, pages 187\u2013201, 1994.","DOI":"10.1007\/BFb0017482"},{"key":"25_CR22","series-title":"Lect Notes Comput Sci","volume-title":"TACAS","author":"Y. Lakhnech","year":"2001","unstructured":"Y. Lakhnech, S. Bensalem, S. Berezin, and S. Owre. Incremental verification by abstraction. In TACAS, volume 2031 of LNCS, 2001."},{"key":"25_CR23","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/S0304-3975(00)00104-3","volume":"256","author":"D. Lesens","year":"2001","unstructured":"D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized networks of processes. Theoretical Computer Science, 256:113\u2013144, 2001.","journal-title":"Theoretical Computer Science"},{"key":"25_CR24","series-title":"Lect Notes Comput Sci","volume-title":"SAS","author":"T. Lev-Ami","year":"2000","unstructured":"T. Lev-Ami and M. Sagiv. TVLA: A system for implementing static analyses. In SAS, volume 1824 of LNCS, 2000."},{"key":"25_CR25","unstructured":"J. Morris. (1) A general axiom of assignment (2) Assignment and linked data structures. In M. Broy and G. Schmidt, editors, Theoretical Foundations of Programming Methodology, 1981."},{"key":"25_CR26","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"K.S. Namjoshi","year":"2000","unstructured":"K.S. Namjoshi and R.P. Kurshan. Syntactic program transformations for automatic abstraction. In CAV, volume 1855 of LNCS, 2000."},{"key":"25_CR27","doi-asserted-by":"crossref","unstructured":"G. Nelson. Verifying reachability invariants of linked structures. In POPL, 1983.","DOI":"10.1145\/567067.567073"},{"key":"25_CR28","doi-asserted-by":"crossref","unstructured":"N. Rinetzky and S. Sagiv. Interprocedural shape analysis for recursive programs. In Computational Complexity, pages 133\u2013149, 2001.","DOI":"10.1007\/3-540-45306-7_10"},{"issue":"3","key":"25_CR29","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. TOPLAS, 24(3):217\u2013298, 2002.","journal-title":"TOPLAS"},{"key":"25_CR30","series-title":"Lect Notes Comput Sci","volume-title":"SAS","author":"D.A. Schmidt","year":"1998","unstructured":"D.A. Schmidt and B. Steffen. Program analysis as model checking of abstract interpretations. In SAS, volume 1503 of LNCS, 1998."},{"key":"25_CR31","doi-asserted-by":"crossref","unstructured":"A. Stump, C.W. Barrett, D.L. Dill, and J.R. Levitt. A decision procedure for an extensional theory of arrays. In LICS, pages 29\u201337, 2001.","DOI":"10.1109\/LICS.2001.932480"},{"key":"25_CR32","unstructured":"http:\/\/www.cs.bell-labs.com\/~kedar\/shape analysis.html ."},{"key":"25_CR33","doi-asserted-by":"crossref","unstructured":"E. Yahav. Verifying safety properties of concurrent Java programs using 3-valued logic. In POPL, pages 27\u201340, 2001.","DOI":"10.1145\/373243.360206"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36384-X_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T00:57:56Z","timestamp":1737593876000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36384-X_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12,16]]},"ISBN":["9783540003489","9783540363842"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-36384-x_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002,12,16]]},"assertion":[{"value":"16 December 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}