{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:59:08Z","timestamp":1725551948581},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540311393"},{"type":"electronic","value":"9783540316220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11609773_14","type":"book-chapter","created":{"date-parts":[[2005,12,12]],"date-time":"2005-12-12T07:28:57Z","timestamp":1134372537000},"page":"207-221","source":"Crossref","is-referenced-by-count":25,"title":["A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs"],"prefix":"10.1007","author":[{"given":"Jesse","family":"Bingham","sequence":"first","affiliation":[]},{"given":"Zvonimir","family":"Rakamari\u0107","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Balaban, I.: personal correspondence (2005)"},{"key":"14_CR2","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.: Shape analysis by predicate abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 164\u2013180. Springer, Heidelberg (2005)"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Conf. on Programming Language Design and Implementation (PLDI), pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/3-540-46002-0_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2002","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 158. Springer, Heidelberg (2002)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-49099-X_2","volume-title":"Programming Languages and Systems","author":"M. Benedikt","year":"1999","unstructured":"Benedikt, M., Reps, T., Sagiv, M.: A decidable logic for describing linked data structures. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol.\u00a01576, p. 2. Springer, Heidelberg (1999)"},{"key":"14_CR6","unstructured":"Bingham, J., Rakamari\u0107, Z.: A logic and decision procedure for predicate abstraction of heap-manipulating programs, UBC Dept. Comp. Sci. Tech Report TR-2005-19 (2005), http:\/\/www.cs.ubc.ca\/cgi-bin\/tr\/2005\/TR-2005-19"},{"issue":"8","key":"14_CR7","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. on Computers"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"R.E. Bryant","year":"2002","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 78\u201392. Springer, Heidelberg (2002)"},{"key":"14_CR9","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. Clarke","year":"2000","unstructured":"Clarke, E., 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":"14_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Symp. on Principles of Programming Languages (POPL), pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"14_CR11","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\u2013323. Springer, Heidelberg (2002)"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Das, S., Dill, D.L.: Successive approximation of abstract transition relations. In: IEEE Symp. on Logic in Computer Science, LICS (2001)","DOI":"10.1109\/LICS.2001.932482"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36126-X_2","volume-title":"Formal Methods in Computer-Aided Design","author":"S. Das","year":"2002","unstructured":"Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517. Springer, Heidelberg (2002)"},{"key":"14_CR14","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":"14_CR15","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Symp. on Principles of Programming Languages (POPL), pp. 191\u2013202 (2002)","DOI":"10.1145\/503272.503291"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","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. Springer, Heidelberg (1997)"},{"key":"14_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of Programming","author":"D. Gries","year":"1981","unstructured":"Gries, D.: The Science of Programming. Springer, New York (1981)"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Symp. on Principles of Programming Languages (POPL), pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-30124-0_15","volume-title":"Computer Science Logic","author":"N. Immerman","year":"2004","unstructured":"Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The boundary between decidability and undecidability for transitive closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 160\u2013174. Springer, Heidelberg (2004)"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Jensen, J.L., J\u00f8rgensen, M.E., Klarlund, N., Schwartzbach, M.I.: Automatic verification of pointer programs using monadic second-order logic. In: Conf. on Programming Language Design and Implementation (PLDI), pp. 226\u2013236 (1997)","DOI":"10.1145\/258915.258936"},{"issue":"1","key":"14_CR21","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":"14_CR22","doi-asserted-by":"crossref","unstructured":"Klarlund, N., Schwartzbach, M.I.: Graph types. In: Symp. on Principles of Programming Languages (POPL), pp. 196\u2013205 (1993)","DOI":"10.1145\/158511.158628"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists, Microsoft Research Tech Report MSR-TR-2005-97 (2005)","DOI":"10.1145\/1111037.1111048"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Reps, T., Sagiv, M., Wilhelm, R.: Putting static analysis to work for verification: A case study. In: Intl. Symp. on Software Testing and Analysis, pp. 26\u201338 (2000)","DOI":"10.1145\/347324.348031"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static Analysis","author":"T. Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 280\u2013301. Springer, Heidelberg (2000)"},{"key":"14_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/11513988_50","volume-title":"Computer Aided Verification","author":"A. Loginov","year":"2005","unstructured":"Loginov, A., Reps, T.W., Sagiv, S.: Abstraction refinement via inductive learning. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 519\u2013533. Springer, Heidelberg (2005)"},{"key":"14_CR27","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":"14_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/11513988_47","volume-title":"Computer Aided Verification","author":"S. McPeak","year":"2005","unstructured":"McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 476\u2013490. Springer, Heidelberg (2005)"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Conf. on Programming Language Design and Implementation (PLDI), pp. 221\u2013231 (2001)","DOI":"10.1145\/378795.378851"},{"key":"14_CR30","unstructured":"Nelson, G.: Techniques for program verification. PhD thesis, Stanford University (1979)"},{"key":"14_CR31","doi-asserted-by":"crossref","unstructured":"Nelson, G.: Verifying reachability invariants of linked structures. In: Symp. on Principles of Programming Languages (POPL), pp. 38\u201347 (1983)","DOI":"10.1145\/567067.567073"},{"issue":"3","key":"14_CR32","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. on Programming Languages and Systems\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"14_CR33","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","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11609773_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T21:28:39Z","timestamp":1683322119000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11609773_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540311393","9783540316220"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/11609773_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}