{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:46:29Z","timestamp":1780994789852,"version":"3.54.1"},"reference-count":73,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2011,12,1]],"date-time":"2011-12-01T00:00:00Z","timestamp":1322697600000},"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":["J. ACM"],"published-print":{"date-parts":[[2011,12]]},"abstract":"<jats:p>The accurate and efficient treatment of mutable data structures is one of the outstanding problem areas in automatic program verification and analysis. Shape analysis is a form of program analysis that attempts to infer descriptions of the data structures in a program, and to prove that these structures are not misused or corrupted. It is one of the more challenging and expensive forms of program analysis, due to the complexity of aliasing and the need to look arbitrarily deeply into the program heap. This article describes a method of boosting shape analyses by defining a compositional method, where each procedure is analyzed independently of its callers. The analysis algorithm uses a restricted fragment of separation logic, and assigns a collection of Hoare triples to each procedure; the triples provide an over-approximation of data structure usage. Our method brings the usual benefits of compositionality---increased potential to scale, ability to deal with incomplete programs, graceful way to deal with imprecision---to shape analysis, for the first time.<\/jats:p>\n          <jats:p>\n            The analysis rests on a generalized form of abduction (inference of explanatory hypotheses), which we call\n            <jats:italic>bi-abduction<\/jats:italic>\n            . Bi-abduction displays abduction as a kind of inverse to the frame problem: it jointly infers anti-frames (missing portions of state) and frames (portions of state not touched by an operation), and is the basis of a new analysis algorithm. We have implemented our analysis and we report case studies on smaller programs to evaluate the quality of discovered specifications, and larger code bases (e.g., sendmail, an imap server, a Linux distribution) to illustrate the level of automation and scalability that we obtain from our compositional method.\n          <\/jats:p>\n          <jats:p>This article makes number of specific technical contributions on proof procedures and analysis algorithms, but in a sense its more important contribution is holistic: the explanation and demonstration of how a massive increase in automation is possible using abductive inference.<\/jats:p>","DOI":"10.1145\/2049697.2049700","type":"journal-article","created":{"date-parts":[[2011,12,13]],"date-time":"2011-12-13T15:45:47Z","timestamp":1323791147000},"page":"1-66","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":166,"title":["Compositional Shape Analysis by Means of Bi-Abduction"],"prefix":"10.1145","volume":"58","author":[{"given":"Cristiano","family":"Calcagno","sequence":"first","affiliation":[{"name":"Monoidics Ltd and Imperial College London"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dino","family":"Distefano","sequence":"additional","affiliation":[{"name":"Queen Mary University of London"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter W.","family":"O\u2019Hearn","sequence":"additional","affiliation":[{"name":"Queen Mary University of London"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[{"name":"University of Oxford"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2011,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_33"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_12"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217943"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification (CAV). 178--192","author":"Berdine J.","unstructured":"Berdine , J. , Calcagno , C. , Cook , B. , Distefano , D. , O\u2019Hearn , P. , Wies , T. , and Yang , H . 2007. Shape analysis of composite data structures . In Proceedings of the 19th International Conference on Computer Aided Verification (CAV). 178--192 . Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P., Wies, T., and Yang, H. 2007. Shape analysis of composite data structures. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV). 178--192."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081741"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_2"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_5"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_13"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2391451.2391478"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480917"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_19"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328469"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Chang B. Rival X. and Necula G. 2007. Shape analysis with structural invariant checkers. In Proceedings of the 14th International Symposium on Static Analysis (SAS). Lecture Notes in Computer Science Springer. 384--401. Chang B. Rival X. and Necula G. 2007. Shape analysis with structural invariant checkers. In Proceedings of the 14th International Symposium on Static Analysis (SAS) . Lecture Notes in Computer Science Springer. 384--401.","DOI":"10.1007\/978-3-540-74061-2_24"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of SSGRR.","author":"Cousot P.","unstructured":"Cousot , P. and Cousot , R . 2001. Compositional separate modular static analysis of programs by abstract interpretation . In Proceedings of SSGRR. Cousot, P. and Cousot, R. 2001. Compositional separate modular static analysis of programs by abstract interpretation. In Proceedings of SSGRR."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/647478.727794"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539704446311"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 18th European Conference on Object-Oriented Programming (ECOOP). 465--490","author":"DeLine R.","unstructured":"DeLine , R. and F\u00e4hndrich , M . 2004. Typestates for objects . In Proceedings of the 18th European Conference on Object-Oriented Programming (ECOOP). 465--490 . DeLine, R. and F\u00e4hndrich, M. 2004. Typestates for objects. In Proceedings of the 18th European Conference on Object-Oriented Programming (ECOOP). 465--490."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12029-9_20"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781149"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/200836.200838"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 18th National Conference on Artificial Intelligence and 14th Conference on Innovative Applications of Artificial Intelligence (AAAI\/IAAI). 62--67","author":"Eiter T.","unstructured":"Eiter , T. and Makino , K . 2002. On computing all abductive explanations . In Proceedings of the 18th National Conference on Artificial Intelligence and 14th Conference on Innovative Applications of Artificial Intelligence (AAAI\/IAAI). 62--67 . Eiter, T. and Makino, K. 2002. On computing all abductive explanations. In Proceedings of the 18th National Conference on Artificial Intelligence and 14th Conference on Innovative Applications of Artificial Intelligence (AAAI\/IAAI). 62--67."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237724"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the International Logic Programming Symposium. The MIT Press, 377--392","author":"Giacobazzi R.","year":"1994","unstructured":"Giacobazzi , R. 1994 . Abductive analysis of modular logic programs . In Proceedings of the International Logic Programming Symposium. The MIT Press, 377--392 . Giacobazzi, R. 1994. Abductive analysis of modular logic programs. In Proceedings of the International Logic Programming Symposium. The MIT Press, 377--392."},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 9th International Conference on Computer Aided Verification (CAV). 68--81","author":"Gopan D.","unstructured":"Gopan , D. and Reps , T . 2007. Low-level library analysis and summarization . In Proceedings of the 9th International Conference on Computer Aided Verification (CAV). 68--81 . Gopan, D. and Reps, T. 2007. Low-level library analysis and summarization. In Proceedings of the 9th International Conference on Computer Aided Verification (CAV). 68--81."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_16"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_14"},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the 16th European Symposium on Programming (ESOP). Lecture Notes in Computer Science","volume":"4421","author":"Gulwani S.","unstructured":"Gulwani , S. and Tiwari , A . 2007. Computing procedure summaries for interprocedural analysis . In Proceedings of the 16th European Symposium on Programming (ESOP). Lecture Notes in Computer Science , vol. 4421 . Springer, 253--267. Gulwani, S. and Tiwari, A. 2007. Computing procedure summaries for interprocedural analysis. In Proceedings of the 16th European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 4421. Springer, 253--267."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328468"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250764"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040331"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0059696"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375634.1375653"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.6.719"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050057"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_49"},{"key":"e_1_2_1_48_1","unstructured":"Lev-Ami T. Sagiv M. Reps T. and Gulwani S. 2007. Backward analysis for inferring quantified preconditions. Tech rep. TR-2007-12-01 Tel-Aviv University. Lev-Ami T. Sagiv M. Reps T. and Gulwani S. 2007. Backward analysis for inferring quantified preconditions. Tech rep. TR-2007-12-01 Tel-Aviv University."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.06.003"},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the 14th International Symposium on Static Analysis (SAS). 419--436","author":"Magill S.","unstructured":"Magill , S. , Berdine , J. , Clarke , E. , and Cook , B . 2007. Arithmetic strengthening for shape analysis . In Proceedings of the 14th International Symposium on Static Analysis (SAS). 419--436 . Magill, S., Berdine, J., Clarke, E., and Cook, B. 2007. Arithmetic strengthening for shape analysis. In Proceedings of the 14th International Symposium on Static Analysis (SAS). 419--436."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_13"},{"key":"e_1_2_1_52_1","volume-title":"Proceedings of the 13th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science","volume":"4424","author":"Manevich R.","unstructured":"Manevich , R. , Berdine , J. , Cook , B. , Ramalingam , G. , and Sagiv , M . 2007. Shape analysis by graph decomposition . In Proceedings of the 13th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science , vol. 4424 . Springer, 3--18. Manevich, R., Berdine, J., Cook, B., Ramalingam, G., and Sagiv, M. 2007. Shape analysis by graph decomposition. In Proceedings of the 13th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 4424. Springer, 3--18."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/1788374.1788396"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.5555\/1787526.1787544"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00215-5"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_34"},{"key":"e_1_2_1_57_1","volume-title":"Proceedings of the 11th International Symposium on Static Analysis (SAS). 165--180","author":"Nystrom E.","unstructured":"Nystrom , E. , Kim , H. , and Hwu , W . 2004. Bottom-up and top-down context-sensitive summary-based pointer analysis . In Proceedings of the 11th International Symposium on Static Analysis (SAS). 165--180 . Nystrom, E., Kim, H., and Hwu, W. 2004. Bottom-up and top-down context-sensitive summary-based pointer analysis. In Proceedings of the 11th International Symposium on Static Analysis (SAS). 165--180."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of the 15th International Workshop on Computer Science Logic (CSL). 1--19","author":"O\u2019Hearn P. W.","unstructured":"O\u2019Hearn , P. W. , Reynolds , J. C. , and Yang , H . 2001. Local reasoning about programs that alter data structures . In Proceedings of the 15th International Workshop on Computer Science Logic (CSL). 1--19 . O\u2019Hearn, P. W., Reynolds, J. C., and Yang, H. 2001. Local reasoning about programs that alter data structures. In Proceedings of the 15th International Workshop on Computer Science Logic (CSL). 1--19."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1498926.1498929"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00849080"},{"key":"e_1_2_1_62_1","volume-title":"Collected Papers of Charles Sanders Peirce","author":"Peirce C.","unstructured":"Peirce , C. 1958. Collected Papers of Charles Sanders Peirce . Harvard University Press . Peirce, C. 1958. Collected Papers of Charles Sanders Peirce. Harvard University Press."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_19"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_31"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040330"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_20"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/271510.271517"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/320384.320400"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_36"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2049697.2049700","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2049697.2049700","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:26:41Z","timestamp":1750278401000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2049697.2049700"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12]]},"references-count":73,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2011,12]]}},"alternative-id":["10.1145\/2049697.2049700"],"URL":"https:\/\/doi.org\/10.1145\/2049697.2049700","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,12]]},"assertion":[{"value":"2010-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-12-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}