{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T06:16:35Z","timestamp":1784873795483,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,1,21]],"date-time":"2009-01-21T00:00:00Z","timestamp":1232496000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2009,1,21]]},"DOI":"10.1145\/1480881.1480917","type":"proceedings-article","created":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T09:41:38Z","timestamp":1232444498000},"page":"289-300","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":119,"title":["Compositional shape analysis by means of bi-abduction"],"prefix":"10.1145","author":[{"given":"Cristiano","family":"Calcagno","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dino","family":"Distefano","sequence":"additional","affiliation":[{"name":"Queen Mary, University of London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"O'Hearn","sequence":"additional","affiliation":[{"name":"Queen Mary, University of London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[{"name":"Queen Mary, University of London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2009,1,21]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_33"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_31"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_12"},{"key":"e_1_3_2_1_4_1","volume-title":"CAV'07","author":"Berdine J.","unstructured":"J. Berdine , C. Calcagno , B. Cook , D. Distefano , P. O'Hearn , T. Wies , and H. Yang . Shape analysis of composite data structures . In CAV'07 . J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. O'Hearn, T. Wies, and H. Yang. Shape analysis of composite data structures. In CAV'07."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_5"},{"key":"e_1_3_2_1_7_1","volume-title":"SAS'07","author":"Calcagno C.","unstructured":"C. Calcagno , D. Distefano , P. O'Hearn , and H. Yang . Footprint analysis: A shape analysis that discovers preconditions . In SAS'07 . C. Calcagno, D. Distefano, P. O'Hearn, and H. Yang. Footprint analysis: A shape analysis that discovers preconditions. In SAS'07."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328469"},{"key":"e_1_3_2_1_9_1","first-page":"384","volume-title":"SAS'07","author":"Chang B.","unstructured":"B. Chang , X. Rival , and G. Necula . Shape analysis with structural invariant checkers . In SAS'07 , pp. 384 -- 401 . B. Chang, X. Rival, and G. Necula. Shape analysis with structural invariant checkers. In SAS'07, pp. 384--401."},{"key":"e_1_3_2_1_10_1","volume-title":"SSGRR'01","author":"Cousot P.","year":"2001","unstructured":"P. Cousot and R. Cousot . Compositional separate modular static analysis of programs by abstract interpretation . In SSGRR'01 .% In Proceedings of SSGRR, Compact disk, L'Aquila, Italy , 2001 . P. Cousot and R. Cousot. Compositional separate modular static analysis of programs by abstract interpretation. In SSGRR'01.% In Proceedings of SSGRR, Compact disk, L'Aquila, Italy, 2001."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781149"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237724"},{"key":"e_1_3_2_1_15_1","first-page":"377","volume-title":"SLP'94","author":"Giacobazzi R.","unstructured":"R. Giacobazzi . Abductive analysis of modular logic programs . In SLP'94 , pp. 377 -- 392 . R. Giacobazzi. Abductive analysis of modular logic programs. In SLP'94, pp. 377--392."},{"key":"e_1_3_2_1_16_1","first-page":"68","volume-title":"CAV'07","author":"Gopan D.","unstructured":"D. Gopan and T. Reps . Low-level library analysis and summarization . In CAV'07 , pp. 68 -- 81 . D. Gopan and T. Reps. Low-level library analysis and summarization. In CAV'07, pp. 68--81."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_16"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250765"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328468"},{"key":"e_1_3_2_1_20_1","first-page":"253","volume-title":"ESOP'07","author":"Gulwani S.","unstructured":"S. Gulwani and A. Tiwari . Computing procedure summaries for interprocedural analysis . In ESOP'07 , pp. 253 -- 267 . S. Gulwani and A. Tiwari. Computing procedure summaries for interprocedural analysis. In ESOP'07, pp. 253--267."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250764"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040331"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_36"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.6.719"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503276"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_49"},{"key":"e_1_3_2_1_28_1","first-page":"419","volume-title":"Arithmetic Strengthening for Shape Analysis. In SAS'07","author":"Magill S.","unstructured":"S. Magill , J. Berdine , E. Clarke , and B. Cook . Arithmetic Strengthening for Shape Analysis. In SAS'07 , pp. 419 -- 436 . S. Magill, J. Berdine, E. Clarke, and B. Cook. Arithmetic Strengthening for Shape Analysis. In SAS'07, pp. 419--436."},{"key":"e_1_3_2_1_29_1","first-page":"3","volume-title":"TACAS'07","author":"Manevich R.","unstructured":"R. Manevich , J. Berdine , B. Cook , G. Ramalingam , and M. Sagiv . Shape analysis by graph decomposition . In TACAS'07 , pp. 3 -- 18 . R. Manevich, J. Berdine, B. Cook, G. Ramalingam, and M. Sagiv. Shape analysis by graph decomposition. In TACAS'07, pp. 3--18."},{"key":"e_1_3_2_1_30_1","first-page":"245","volume-title":"CC'08","author":"Marron M.","unstructured":"M. Marron , M. Hermenegildo , D. Kapur , and D. Stefanovic . Efficient context-sensitive shape analysis with graph based heap models . In CC'08 , pp. 245 -- 259 . M. Marron, M. Hermenegildo, D. Kapur, and D. Stefanovic. Efficient context-sensitive shape analysis with graph based heap models. In CC'08, pp. 245--259."},{"key":"e_1_3_2_1_31_1","first-page":"188","volume-title":"VMCAI'08","author":"Moy Y.","unstructured":"Y. Moy . Sufficient preconditions for modular assertion checking . In VMCAI'08 , pp. 188 -- 202 . Y. Moy. Sufficient preconditions for modular assertion checking. In VMCAI'08, pp. 188--202."},{"key":"e_1_3_2_1_32_1","volume-title":"VMCAI'07","author":"Nguyen H.","unstructured":"H. Nguyen , C. David , S. Qin , and W.-N. Chin . Automated verification of shape and size propertiesvia separation logic . In VMCAI'07 . H. Nguyen, C. David, S. Qin, and W.-N. Chin. Automated verification of shape and size propertiesvia separation logic. In VMCAI'07."},{"key":"e_1_3_2_1_33_1","first-page":"165","volume-title":"SAS'04","author":"Nystrom E.","unstructured":"E. Nystrom , H. Kim , and W. Hwu . Bottom-up and top-down context-sensitive summary-based pointer analysis . SAS'04 , pp. 165 -- 180 . E. Nystrom, H. Kim, and W. Hwu. Bottom-up and top-down context-sensitive summary-based pointer analysis. SAS'04, pp. 165--180."},{"key":"e_1_3_2_1_34_1","first-page":"1","volume-title":"CSL'01","author":"O'Hearn P.","unstructured":"P. O'Hearn , J. Reynolds , and H. Yang . Local reasoning about programs that alter data structures . In CSL'01 , pp. 1 -- 19 . P. O'Hearn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In CSL'01, pp. 1--19."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964024"},{"key":"e_1_3_2_1_36_1","volume-title":"Harvard University Press.","author":"Peirce C.","year":"1958","unstructured":"C. Peirce . Collected papers of Charles Sanders Peirce . Harvard University Press. , 1958 . C. Peirce. Collected papers of Charles Sanders Peirce. Harvard University Press., 1958."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_19"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_31"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_3_2_1_40_1","first-page":"55","volume-title":"LICS'02","author":"Reynolds J. C.","unstructured":"J. C. Reynolds . Separation logic : A logic for shared mutable data structures . In LICS'02 , pp. 55 -- 74 . J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS'02, pp. 55--74."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040330"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_20"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/271510.271517"},{"key":"e_1_3_2_1_44_1","volume-title":"Program Flow Analysis: Theory and Applications","author":"Sharir M.","year":"1981","unstructured":"M. Sharir and A. Pnueli . Two approaches to interprocedural data flow analysis . In S. Muchnick and J. Jones, editors, Program Flow Analysis: Theory and Applications . Prentice-Hall , 1981 . M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis. In S. Muchnick and J. Jones, editors, Program Flow Analysis: Theory and Applications. Prentice-Hall, 1981."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/320384.320400"}],"event":{"name":"POPL09: The 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Savannah GA USA","acronym":"POPL09","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1480881.1480917","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1480881.1480917","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:29:59Z","timestamp":1750238999000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1480881.1480917"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1,21]]},"references-count":44,"alternative-id":["10.1145\/1480881.1480917","10.1145\/1480881"],"URL":"https:\/\/doi.org\/10.1145\/1480881.1480917","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1594834.1480917","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2009,1,21]]},"assertion":[{"value":"2009-01-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}