{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:06:21Z","timestamp":1767927981174,"version":"3.49.0"},"reference-count":70,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2023,5,15]],"date-time":"2023-05-15T00:00:00Z","timestamp":1684108800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Amazon and a Discovery Partners Institute"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2023,6,30]]},"abstract":"<jats:p>\n            We propose a novel logic,\n            <jats:italic>Frame Logic<\/jats:italic>\n            (FL), that extends first-order logic and recursive definitions with a construct\n            <jats:italic>Sp<\/jats:italic>\n            (\u00b7) that captures the\n            <jats:italic>implicit supports<\/jats:italic>\n            of formulas\u2014the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a\n            <jats:italic>precise<\/jats:italic>\n            fragment of separation logic to frame logic. Finally, we design a program logic based on frame logic for reasoning with programs that dynamically update heaps that facilitates local specifications and frame reasoning. This program logic consists of both localized proof rules as well as rules that derive the weakest tightest preconditions in frame logic.\n          <\/jats:p>","DOI":"10.1145\/3583057","type":"journal-article","created":{"date-parts":[[2023,2,9]],"date-time":"2023-02-09T13:47:00Z","timestamp":1675950420000},"page":"1-44","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A First-order Logic with Frames"],"prefix":"10.1145","volume":"45","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6311-1467","authenticated-orcid":false,"given":"Adithya","family":"Murali","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Department of Computer Science, Urbana, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1898-439X","authenticated-orcid":false,"given":"Lucas","family":"Pe\u00f1a","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Department of Computer Science, Urbana, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1529-2806","authenticated-orcid":false,"given":"Christof","family":"L\u00f6ding","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Department of Computer Science, Aachen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9782-721X","authenticated-orcid":false,"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Department of Computer Science, Urbana, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,5,15]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567763"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_3_2_4_2","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1007\/978-3-540-87873-5_16","volume-title":"Verified Software: Theories, Tools, Experiments","author":"Banerjee Anindya","year":"2008","unstructured":"Anindya Banerjee, Mike Barnett, and David A. Naumann. 2008. Boogie meets regions: A verification experience report. In Verified Software: Theories, Tools, Experiments, Natarajan Shankar and Jim Woodcock (Eds.). Springer Berlin, 177\u2013191."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/2485981"},{"key":"e_1_3_2_6_2","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1007\/978-3-540-70592-5_17","volume-title":"ECOOP 2008\u2014Object-Oriented Programming","author":"Banerjee Anindya","year":"2008","unstructured":"Anindya Banerjee, David A. Naumann, and Stan Rosenberg. 2008. Regional logic for local reasoning about global invariants. In ECOOP 2008\u2014Object-Oriented Programming, Jan Vitek (Ed.). Springer Berlin, 387\u2013411."},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/2485982"},{"key":"e_1_3_2_8_2","first-page":"364","volume-title":"Formal Methods for Components and Objects","author":"Barnett Mike","year":"2005","unstructured":"Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects, Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (Eds.). Springer Berlin, 364\u2013387."},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_3_2_12_2","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-642-34281-3_14","volume-title":"Formal Methods and Software Engineering","author":"Bobot Fran\u00e7ois","year":"2012","unstructured":"Fran\u00e7ois Bobot and Jean-Christophe Filli\u00e2tre. 2012. Separation predicates: A taste of separation logic in first-order logic. In Formal Methods and Software Engineering, Toshiaki Aoki and Kenji Taguchi (Eds.). Springer Berlin, 167\u2013181."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.469460"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/24.2.148"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_24"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.5555\/2032266.2032278"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.5555\/646839.708666"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1980.41"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2007.17"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.5555\/2040235.2040256"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1080\/11663081.2015.1018801"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44957-4_47"},{"key":"e_1_3_2_24_2","first-page":"22","volume-title":"Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201914)","author":"Denecker Marc","year":"2014","unstructured":"Marc Denecker and Joost Vennekens. 2014. The well-founded semantics is the principle of inductive definition, revisited. In Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201914). AAAI Press, 22\u201331."},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.021"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-934613-03-3.50020-9"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429131"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802187"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535854"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3- 642-39799-8_53"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_3"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_2_35_2","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/978-3-642-54108-7_11","volume-title":"Verified Software: Theories, Tools, Experiments","author":"Jost Daniel","year":"2014","unstructured":"Daniel Jost and Alexander J. Summers. 2014. An automatic encoding from VeriFast predicates into implicit dynamic frames. In Verified Software: Theories, Tools, Experiments, Ernie Cohen and Andrey Rybalchenko (Eds.). Springer Berlin, 202\u2013221."},{"key":"e_1_3_2_36_2","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/11813040_19","volume-title":"FM 2006: Formal Methods","author":"Kassios Ioannis T.","year":"2006","unstructured":"Ioannis T. Kassios. 2006. Dynamic frames: Support for framing, dependencies and sharing without restrictions. In FM 2006: Formal Methods, Jayadev Misra, Tobias Nipkow, and Emil Sekerinski (Eds.). Springer-Verlag, Berlin, 268\u2013283."},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0152-5"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009887"},{"key":"e_1_3_2_39_2","first-page":"1","volume-title":"Computer Aided Verification","author":"Kov\u00e1cs Laura","year":"2013","unstructured":"Laura Kov\u00e1cs and Andrei Voronkov. 2013. First-order theorem proving and Vampire. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin, 1\u201335."},{"key":"e_1_3_2_40_2","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1007\/978-3-030-44914-8_12","volume-title":"Programming Languages and Systems","author":"Krishna Siddharth","year":"2020","unstructured":"Siddharth Krishna, Alexander J. Summers, and Thomas Wies. 2020. Local reasoning for global graph properties. In Programming Languages and Systems, Peter M\u00fcller (Ed.). Springer International Publishing, Cham, 308\u2013335."},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481874"},{"key":"e_1_3_2_42_2","first-page":"592","volume-title":"Computer Aided Verification","author":"Lee Oukseh","year":"2011","unstructured":"Oukseh Lee, Hongseok Yang, and Rasmus Petersen. 2011. Program analysis for overlaid data structures. In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin, 592\u2013608."},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07003-1"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158098"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103673"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563354"},{"key":"e_1_3_2_50_2","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1007\/978-3-030-44914-8_19","volume-title":"Programming Languages and Systems","author":"Murali Adithya","year":"2020","unstructured":"Adithya Murali, Lucas Pe\u00f1a, Christof L\u00f6ding, and P. Madhusudan. 2020. A first-order logic with frames. In Programming Languages and Systems, Peter M\u00fcller (Ed.). Springer International Publishing, Cham, 515\u2013543."},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993563"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-028-4-286"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964024"},{"key":"e_1_3_2_55_2","volume-title":"Decision Procedures for Separation Logic: Beyond Symbolic Heaps","author":"Pagel Jens","year":"2020","unstructured":"Jens Pagel. 2020. Decision Procedures for Separation Logic: Beyond Symbolic Heaps. Ph.D. Dissertation. Wien."},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040326"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_23"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594325"},{"key":"e_1_3_2_59_2","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1007\/978-3-319-03542-0_7","volume-title":"Programming Languages and Systems (APLAS)","author":"P\u00e9rez Juan Antonio Navarro","year":"2013","unstructured":"Juan Antonio Navarro P\u00e9rez and Andrey Rybalchenko. 2013. Separation logic modulo theories. In Programming Languages and Systems (APLAS). Springer International Publishing, Cham, 90\u2013106."},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_54"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_47"},{"key":"e_1_3_2_62_2","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/978-3-642-54862-8_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Piskac Ruzica","year":"2014","unstructured":"Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014. GRASShopper. In Tools and Algorithms for the Construction and Analysis of Systems, Erika \u00c1brah\u00e1m and Klaus Havelund (Eds.). Springer Berlin, 124\u2013139."},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462169"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-021-00628-w"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160911"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706325"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_40"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802186"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3583057","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3583057","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:48:47Z","timestamp":1750182527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3583057"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,15]]},"references-count":70,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,6,30]]}},"alternative-id":["10.1145\/3583057"],"URL":"https:\/\/doi.org\/10.1145\/3583057","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,5,15]]},"assertion":[{"value":"2020-05-30","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-10-26","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-05-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}