{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T05:55:30Z","timestamp":1770270930772,"version":"3.49.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-01-1-0796N00014-01-1-0708"],"award-info":[{"award-number":["N00014-01-1-0796N00014-01-1-0708"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCR-9986308CCF-0540955CCF-0524051"],"award-info":[{"award-number":["CCR-9986308CCF-0540955CCF-0524051"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCR-9986308CCF-0540955CCF-0524051"],"award-info":[{"award-number":["CCR-9986308CCF-0540955CCF-0524051"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2010,1]]},"abstract":"<jats:p>\n            This article addresses the verification of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued fields, that is,\n            <jats:italic>interprocedural shape analysis<\/jats:italic>\n            . The article makes three contributions.\n          <\/jats:p>\n          <jats:p>\u2014 It introduces a new method for abstracting relations over memory configurations for use in abstract interpretation.<\/jats:p>\n          <jats:p>\u2014 It shows how this method furnishes the elements needed for a compositional approach to shape analysis. In particular, abstracted relations are used to represent the shape transformation performed by a sequence of operations, and an overapproximation to relational composition can be performed using the meet operation of the domain of abstracted relations.<\/jats:p>\n          <jats:p>\n            \u2014 It applies these ideas in a new algorithm for context-sensitive interprocedural shape analysis. The algorithm creates procedure summaries using abstracted relations over memory configurations, and the meet-based composition operation provides a way to apply the summary transformer for a procedure\n            <jats:italic>P<\/jats:italic>\n            at each call site from which\n            <jats:italic>P<\/jats:italic>\n            is called.\n          <\/jats:p>\n          <jats:p>The algorithm has been applied successfully to establish properties of both (i) recursive programs that manipulate lists and (ii) recursive programs that manipulate binary trees.<\/jats:p>","DOI":"10.1145\/1667048.1667050","type":"journal-article","created":{"date-parts":[[2010,8,24]],"date-time":"2010-08-24T13:16:40Z","timestamp":1282655800000},"page":"1-52","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["A relational approach to interprocedural shape analysis"],"prefix":"10.1145","volume":"32","author":[{"given":"Bertrand","family":"Jeannet","sequence":"first","affiliation":[{"name":"INRIA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexey","family":"Loginov","sequence":"additional","affiliation":[{"name":"GrammaTech, Inc."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel Aviv University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2010,2,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_14"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_3"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/379605.379690"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_2_1_5_1","unstructured":"Bogudlov I. Lev-Ami T. Reps T. and Sagiv M. 2007a. Revamping TVLA: Making parametric shape analysis competitive. Tech. rep. TR-2007--01-01 Tel-Aviv University Tel-Aviv Israel.  Bogudlov I. Lev-Ami T. Reps T. and Sagiv M. 2007a. Revamping TVLA: Making parametric shape analysis competitive. Tech. rep. TR-2007--01-01 Tel-Aviv University Tel-Aviv Israel."},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the International Conference on Computer Aided Verification. Lecture Notes in Computer Science","volume":"4590","author":"Bogudlov I.","unstructured":"Bogudlov , I. , Lev-Ami , T. , Reps , T. , and Sagiv , M . 2007b. Revamping TVLA: Making parametric shape analysis competitive (tool paper) . In Proceedings of the International Conference on Computer Aided Verification. Lecture Notes in Computer Science , vol. 4590 , Springer. Bogudlov, I., Lev-Ami, T., Reps, T., and Sagiv, M. 2007b. Revamping TVLA: Making parametric shape analysis competitive (tool paper). In Proceedings of the International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 4590, Springer."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/646732.701281"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604137"},{"key":"e_1_2_1_9_1","unstructured":"Clarke Jr. E. Grumberg O. and Peled D. 1999. Model Checking. The MIT Press.   Clarke Jr. E. Grumberg O. and Peled D. 1999. Model Checking. The MIT Press."},{"key":"e_1_2_1_10_1","unstructured":"Cousot P. and Cousot R. 1977. Static determination of dynamic properties of recursive procedures. In Formal Descriptions of Programming Concepts E. Neuhold Ed. North-Holland 237--277.  Cousot P. and Cousot R. 1977. Static determination of dynamic properties of recursive procedures. In Formal Descriptions of Programming Concepts E. Neuhold Ed. North-Holland 237--277."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Finkel A. B. Willems and Wolper P. 1997. A direct symbolic approach to model checking pushdown systems. Electron. Notes Theor. Comput. Sci. 9.  Finkel A. B. Willems and Wolper P. 1997. A direct symbolic approach to model checking pushdown systems. Electron. Notes Theor. Comput. Sci. 9.","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_38"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_16"},{"key":"e_1_2_1_15_1","volume-title":"The Science of Programming","author":"Gries D.","unstructured":"Gries , D. 1981. The Science of Programming . Springer . Gries, D. 1981. The Science of Programming. Springer."},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the Static Analysis Symposium (SAS'04)","volume":"3148","author":"Jeannet B.","unstructured":"Jeannet , B. , Loginov , A. , Reps , T. , and Sagiv , M . 2004. A relational approach to interprocedural shape analysis . In Proceedings of the Static Analysis Symposium (SAS'04) . Lecture Notes in Computer Science , vol. 3148 , Springer. Jeannet, B., Loginov, A., Reps, T., and Sagiv, M. 2004. A relational approach to interprocedural shape analysis. In Proceedings of the Static Analysis Symposium (SAS'04). Lecture Notes in Computer Science, vol. 3148, Springer."},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the Workshop on Algebraic Methodology and Software Technology (AMAST'04)","volume":"3116","author":"Jeannet B.","unstructured":"Jeannet , B. and Serwe , W . 2004. Abstracting call-stacks for interprocedural verification of imperative programs . In Proceedings of the Workshop on Algebraic Methodology and Software Technology (AMAST'04) . Lecture Notes in Computer Science , vol. 3116 , Springer. Jeannet, B. and Serwe, W. 2004. Abstracting call-stacks for interprocedural verification of imperative programs. In Proceedings of the Workshop on Algebraic Methodology and Software Technology (AMAST'04). Lecture Notes in Computer Science, vol. 3116, Springer."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/647471.727286"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328461"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/347324.348031"},{"key":"e_1_2_1_21_1","series-title":"Lecture Notes in Computer Science","volume-title":"TVLA: A system for implementing static analyses. In Proceedings of the Static Analysis Symposium (SAS'00)","author":"Lev-Ami T.","year":"2000","unstructured":"Lev-Ami , T. and Sagiv , M . 2000 . TVLA: A system for implementing static analyses. In Proceedings of the Static Analysis Symposium (SAS'00) . Lecture Notes in Computer Science , vol. 1824 , Springer , 280--301. Lev-Ami, T. and Sagiv, M. 2000. TVLA: A system for implementing static analyses. In Proceedings of the Static Analysis Symposium (SAS'00). Lecture Notes in Computer Science, vol. 1824, Springer, 280--301."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_50"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A. 1995. Temporal Verification of Reactive Systems: Safety Springer.   Manna Z. and Pnueli A. 1995. Temporal Verification of Reactive Systems: Safety Springer.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1788374.1788396"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765712.1765740"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.009"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040330"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/647477.727768"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_20"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00072-2"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_2_1_37_1","first-page":"189","article-title":"Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, Eds. Prentice-Hall, Englewood Cliffs","volume":"7","author":"Sharir M.","year":"1981","unstructured":"Sharir , M. and Pnueli , A. 1981 . Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, Eds. Prentice-Hall, Englewood Cliffs , NJ. Chapter 7 , 189 -- 234 . Sharir, M. and Pnueli, A. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, Eds. Prentice-Hall, Englewood Cliffs, NJ. Chapter 7, 189--234.","journal-title":"NJ. Chapter"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_39"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1667048.1667050","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1667048.1667050","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:41:30Z","timestamp":1750250490000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1667048.1667050"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,1]]}},"alternative-id":["10.1145\/1667048.1667050"],"URL":"https:\/\/doi.org\/10.1145\/1667048.1667050","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,1]]},"assertion":[{"value":"2008-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-02-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}