{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T13:28:04Z","timestamp":1726406884312},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540377566"},{"type":"electronic","value":"9783540377580"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11823230_13","type":"book-chapter","created":{"date-parts":[[2006,8,17]],"date-time":"2006-08-17T13:46:30Z","timestamp":1155822390000},"page":"182-203","source":"Crossref","is-referenced-by-count":40,"title":["Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic"],"prefix":"10.1007","author":[{"given":"Cristiano","family":"Calcagno","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dino","family":"Distefano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter W.","family":"O\u2019Hearn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_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":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/11823230_15","volume-title":"Static Analysis","author":"G. Balakrishnan","year":"2006","unstructured":"Balakrishnan, G., Reps, T.: Recency-Abstraction for Heap-Allocated Storage. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 221\u2013239. Springer, Heidelberg (2006)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J. Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 52\u201368. Springer, Heidelberg (2005)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11804192_6","volume-title":"Formal Methods for Components and Objects","author":"J. Berdine","year":"2006","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 115\u2013137. Springer, Heidelberg (2006)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/11817963_35","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2006","unstructured":"Berdine, J., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 386\u2013400. Springer, Heidelberg (2006)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-540-31980-1_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., Habermehl, P., Moro, P., Vojnar, T.: Verifying programs with dynamic 1-selector-linked structures in regular model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 13\u201329. Springer, Heidelberg (2005)"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Chase, D., Wegman, M., Zadeck, F.: Analysis of pointers and structures. In: PLDI, pp. 296\u2013310 (1990)","DOI":"10.1145\/93542.93585"},{"issue":"6","key":"13_CR8","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1145\/512274.512288","volume":"7","author":"W.T. Comfort","year":"1964","unstructured":"Comfort, W.T.: Multiword list items. CACM\u00a07(6), 357\u2013362 (1964)","journal-title":"CACM"},{"key":"13_CR9","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: 4th POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: 6th POPL, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"issue":"4","key":"13_CR11","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Log. Comput.\u00a02(4), 511\u2013547 (1992)","journal-title":"J. Log. Comput."},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTRE\u00c9 analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: 5th POPL, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-540-30538-5_21","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"D. Distefano","year":"2004","unstructured":"Distefano, D., Katoen, J.-P., Rensink, A.: Who is pointing when to whom? On the automated verification of linked list structures. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 250\u2013262. Springer, Heidelberg (2004)"},{"key":"13_CR15","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. LNCS, vol.\u00a03920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Dor, N., Rodeh, M., Sagiv, M.: Towards a realistic tool for statically detecting all buffer overflows in C. In: PLDI, pp. 155\u2013167 (2003)","DOI":"10.1145\/780822.781149"},{"key":"13_CR17","unstructured":"Eo, H., Yi, K., Eom, H.: Differential fixpoint iteration with subtraction for non-distributive program analysis (submitted, 2006)"},{"key":"13_CR18","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)"},{"key":"13_CR19","volume-title":"The C Programming Language","author":"B.W. Kernighan","year":"1988","unstructured":"Kernighan, B.W., Ritchie, D.M.: The C Programming Language, 2nd edn. Prentice-Hall, New Jersey (1988)","edition":"2"},{"key":"13_CR20","series-title":"Fundamental Algorithms","volume-title":"The Art of Computer Programming","author":"D.E. Knuth","year":"1973","unstructured":"Knuth, D.E.: The Art of Computer Programming, 2nd edn. Fundamental Algorithms, vol.\u00a0I. Addison-Wesley, Reading (1973)","edition":"2"},{"key":"13_CR21","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":"13_CR22","unstructured":"Magill, S., Nanevski, A., Clarke, E., Lee, P.: Inferring invariants in Separation Logic for imperative list-processing programs. In: 3rd SPACE Workshop (2006)"},{"key":"13_CR23","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":"13_CR24","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":"13_CR25","doi-asserted-by":"crossref","unstructured":"Marti, N., Affeldt, R., Yonezawa, A.: Verification of the heap manager of an operating system using separation logic. In: 3rd SPACE Workshop (2006)","DOI":"10.1007\/11901433_22"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Reps, T., Balakrishnan, G., Lim, J.: Intermediate-representation recovery from low-level code. In: PEPM 2006, pp. 100\u2013111 (2006)","DOI":"10.1145\/1111542.1111560"},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th LICS, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"13_CR28","unstructured":"Xavier Rival. Personal communication (2005)"},{"issue":"2","key":"13_CR29","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1145\/1057387.1057388","volume":"27","author":"R. Rugina","year":"2005","unstructured":"Rugina, R., Rinard, M.: Symbolic bounds analysis of pointers, array indices, and accessed memory regions. ACM TOPLAS\u00a027(2), 185\u2013235 (2005)","journal-title":"ACM TOPLAS"},{"issue":"1","key":"13_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/271510.271517","volume":"20","author":"M. Sagiv","year":"1998","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM TOPLAS\u00a020(1), 1\u201350 (1998)","journal-title":"ACM TOPLAS"},{"issue":"3","key":"13_CR31","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 3valued logic. ACM TOPLAS\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM TOPLAS"},{"key":"13_CR32","unstructured":"Wagner, D., Foster, J., Brewer, E., Aiken, A.: A first step towards automated detection of buffer overrun vulnerabilities. In: Proceedings of NDSS (2000)"},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-36575-3_25","volume-title":"Programming Languages and Systems","author":"D. Yu","year":"2003","unstructured":"Yu, D., Hamid, N.A., Shao, Z.: Building certified libraries for PCC: Dynamic storage allocation. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 363\u2013379. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11823230_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:17:01Z","timestamp":1605644221000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11823230_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540377566","9783540377580"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/11823230_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}