{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:56:23Z","timestamp":1725512183029},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540713159"},{"type":"electronic","value":"9783540713227"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71322-7_12","type":"book-chapter","created":{"date-parts":[[2007,6,4]],"date-time":"2007-06-04T15:05:59Z","timestamp":1180969559000},"page":"247-272","source":"Crossref","is-referenced-by-count":3,"title":["Refinement-Based Verification for Possibly-Cyclic Lists"],"prefix":"10.1007","author":[{"given":"Alexey","family":"Loginov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Distefano, D., O\u2019Hearn, P., Yang, H.: Interprocedural shape analysis with separated heap abstractions. In: Tools and Algs. for the Construction and Analysis of Systems, March 2006, pp. 287\u2013302 (2006)","key":"12_CR1","DOI":"10.1007\/11691372_19"},{"issue":"1","key":"12_CR2","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/344788.344808","volume":"29","author":"G. Dong","year":"2000","unstructured":"Dong, G., Su, J.: Incremental maintenance of recursive views using relational calculus\/SQL. SIGMOD Record\u00a029(1), 44\u201351 (2000)","journal-title":"SIGMOD Record"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/11823230_16","volume-title":"Static Analysis","author":"A. Gotsman","year":"2006","unstructured":"Gotsman, A., Berdine, J., Cook, B.: Interprocedural shape analysis with separated heap abstractions. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 240\u2013260. Springer, Heidelberg (2006)"},{"unstructured":"Hesse, W.: Dynamic Computational Complexity. PhD thesis, Dept. of Computer Science, University of Massachusetts (June 2003)","key":"12_CR4"},{"doi-asserted-by":"crossref","unstructured":"Immerman, N., et al.: The boundary between decidability and undecidability for transitive closure logics. In: Workshop on Computer Science Logic, September 2004, pp. 160\u2013174 (2004)","key":"12_CR5","DOI":"10.1007\/978-3-540-30124-0_15"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., et al.: Verification via structure simulation. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 281\u2013294. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Klarlund, N., Schwartzbach, M.: Graph types. In: Symp. on Principles of Programming Languages (January 1993)","key":"12_CR7","DOI":"10.1145\/158511.158628"},{"doi-asserted-by":"crossref","unstructured":"Lahiri, S., Qadeer, S.: Verifying properties of well-founded linked lists. In: Symp. on Principles of Programming Languages, January 2006, pp. 115\u2013126 (2006)","key":"12_CR8","DOI":"10.1145\/1111037.1111048"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/11513988_50","volume-title":"Computer Aided Verification","author":"A. Loginov","year":"2005","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Abstraction refinement via inductive learning. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 519\u2013533. Springer, Heidelberg (2005)"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., et al.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 181\u2013198. Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.: The pointer assertion logic engine. In: Conf. on Programming Language Design and Impl., June 2001, pp. 221\u2013231 (2001)","key":"12_CR12","DOI":"10.1145\/381694.378851"},{"doi-asserted-by":"crossref","unstructured":"Nelson, G.: Verifying reachability invariants of linked structures. In: Symp. on Principles of Programming Languages, January 1983, pp. 38\u201347 (1983)","key":"12_CR13","DOI":"10.1145\/567067.567073"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/3-540-36575-3_26","volume-title":"Programming Languages and Systems","author":"T. Reps","year":"2003","unstructured":"Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol.\u00a02618, pp. 380\u2013398. Springer, Heidelberg (2003)"},{"doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation Logic: A logic for shared mutable data structures. In: Symp. on Logic in Computer Science, July 2002, pp. 55\u201374 (2002)","key":"12_CR15","DOI":"10.1109\/LICS.2002.1029817"},{"doi-asserted-by":"crossref","unstructured":"Rinetzky, N., et al.: A semantics for procedure local heaps and its abstractions. In: Symp. on Principles of Programming Languages, January 2005, pp. 296\u2013309 (2005)","key":"12_CR16","DOI":"10.1145\/1040305.1040330"},{"issue":"3","key":"12_CR17","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. TOPLAS\u00a024(3), 217\u2013298 (2002)","journal-title":"TOPLAS"},{"unstructured":"Yorsh, G., et al.: Logical characterizations of heap abstractions. To appear in ACM Transactions on Computational Logic (TOCL)","key":"12_CR18"}],"container-title":["Lecture Notes in Computer Science","Program Analysis and Compilation, Theory and Practice"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71322-7_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:18:28Z","timestamp":1605763108000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71322-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540713159","9783540713227"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71322-7_12","relation":{},"subject":[]}}