{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:14:24Z","timestamp":1763468064359,"version":"3.41.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2011,11,1]],"date-time":"2011-11-01T00:00:00Z","timestamp":1320105600000},"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":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2011,11]]},"abstract":"<jats:p>In this article, we present a new shape analysis algorithm. The key distinguishing aspect of our algorithm is that it is completely compositional, bottom-up and noniterative. We present our algorithm as an inference system for computing Hoare triples summarizing heap manipulating programs. Our inference rules are compositional: Hoare triples for a compound statement are computed from the Hoare triples of its component statements. These inference rules are used as the basis for bottom-up shape analysis of programs.<\/jats:p>\n          <jats:p>Specifically, we present a Logic of Iterated Separation Formulae (LISF), which uses the iterated separating conjunct of Reynolds [2002] to represent program states. A key ingredient of our inference rules is a strong bi-abduction operation between two logical formulas. We describe sound strong bi-abduction and satisfiability procedures for LISF.<\/jats:p>\n          <jats:p>\n            We have built a tool called S\n            <jats:sc>p<\/jats:sc>\n            I\n            <jats:sc>n<\/jats:sc>\n            E that implements these inference rules and have evaluated it on standard shape analysis benchmark programs. Our experiments show that S\n            <jats:sc>p<\/jats:sc>\n            I\n            <jats:sc>n<\/jats:sc>\n            E can generate expressive summaries, which are complete functional specifications in many cases.\n          <\/jats:p>","DOI":"10.1145\/2039346.2039349","type":"journal-article","created":{"date-parts":[[2011,11,21]],"date-time":"2011-11-21T19:54:36Z","timestamp":1321905276000},"page":"1-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Bottom-up shape analysis using LISF"],"prefix":"10.1145","volume":"33","author":[{"given":"Bhargav S.","family":"Gulavani","sequence":"first","affiliation":[{"name":"IIT Bombay, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Supratik","family":"Chakraborty","sequence":"additional","affiliation":[{"name":"IIT Bombay, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Ramalingam","sequence":"additional","affiliation":[{"name":"Microsoft Research India, Bangalore, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aditya V.","family":"Nori","sequence":"additional","affiliation":[{"name":"Microsoft Research India, Bangalore, India"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,11,23]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_33"},{"volume-title":"Proceedings of the International Conference on Concurrency Theory (CONCUR). Springer, 35--48","author":"Abdulla P. A.","key":"e_1_2_1_2_1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11562948_35"},{"volume-title":"Proceedings of the International Conference on Computer Aided Verification (CAV). 178--192","author":"Berdine J.","key":"e_1_2_1_4_1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_17"},{"volume-title":"Proceedings of the International Conference on Computer Aided Verification (CAV). Springer, 223--235","author":"Boigelot B.","key":"e_1_2_1_6_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_2"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_5"},{"volume-title":"Proceedings of the International Conference on Computer Aided Verification (CAV). Springer, 372--386","author":"Bouajjani A.","key":"e_1_2_1_9_1"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480917"},{"volume-title":"Proceedings of the International Symposium on Static Analysis (SAS). 402--418","author":"Calcagno C.","key":"e_1_2_1_11_1"},{"key":"e_1_2_1_12_1","first-page":"843","article-title":"Methods and logics for proving programs. In Formal Models and Semantics, J. van Leeuwen, Ed., Handbook of Theoretical Computer Science, vol. B. Elsevier Science Publishers B.V","volume":"15","author":"Cousot P.","year":"1990","journal-title":"Chapter"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19"},{"key":"e_1_2_1_14_1","unstructured":"Gulavani B. S. Chakraborty S. Ramalingam G. and Nori A. V. 2009. Bottom-up shape analysis using lisf. Tech. rep. TR-09-31 CFDVS IIT Bombay. www.cfdvs.iitb.ac.in\/~bhargav\/spine.html.  Gulavani B. S. Chakraborty S. Ramalingam G. and Nori A. V. 2009. Bottom-up shape analysis using lisf. Tech. rep. TR-09-31 CFDVS IIT Bombay. www.cfdvs.iitb.ac.in\/~bhargav\/spine.html."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250764"},{"volume-title":"Proceedings of the International Symposium on Static Analysis (SAS). 246--264","author":"Jeannet B.","key":"e_1_2_1_16_1"},{"key":"e_1_2_1_17_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_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_31"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040330"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_20"},{"volume":"2027","volume-title":"Proceedings of the Conference on Computer Construction (CC). Lecture Notes in Computer Science","author":"Rinetzky N.","key":"e_1_2_1_24_1"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00187-2"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11690634_7"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2039346.2039349","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2039346.2039349","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:48:54Z","timestamp":1750240134000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2039346.2039349"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11]]},"references-count":27,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2011,11]]}},"alternative-id":["10.1145\/2039346.2039349"],"URL":"https:\/\/doi.org\/10.1145\/2039346.2039349","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2011,11]]},"assertion":[{"value":"2009-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-11-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}