{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:28:18Z","timestamp":1784255298647,"version":"3.55.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>Applications like program synthesis sometimes require proving that a property holds for all of the infinitely many programs described by a grammar---i.e., an inductively defined set of programs. \n \n \n \n \n \n \n \nCurrent verification frameworks overapproximate programs' behavior when sets of programs contain loops, including two Hoare-style logics that fail to be relatively complete when loops are allowed. In this work, we prove that compositionally verifying simple properties for infinite sets of programs requires tracking distinct program behaviors over unboundedly many executions. \n \n \n \n \n \n \n \nTracking this information is both necessary and sufficient for verification. \n \n \n \n \n \n \n \nWe prove this fact in a general, reusable theory of denotational semantics that can model the expressivity and compositionality of verification techniques over infinite sets of programs. \n \n \n \n \n \n \n \nWe construct the minimal compositional semantics that captures simple properties of sets of programs and use it to derive the first sound and relatively complete Hoare-style logic for infinite sets of programs. \n \n \n \n \n \n \n \nThus, our methods can be used to design minimally complex, compositional verification techniques for sets of programs.<\/jats:p>","DOI":"10.1145\/3720515","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"844-870","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Semantics of Sets of Programs"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3897-1828","authenticated-orcid":false,"given":"Jinwoo","family":"Kim","sequence":"first","affiliation":[{"name":"University of California-San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8015-5421","authenticated-orcid":false,"given":"Shaan","family":"Nagy","sequence":"additional","affiliation":[{"name":"University of California-San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5676-9949","authenticated-orcid":false,"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9625-4037","authenticated-orcid":false,"given":"Loris","family":"D'Antoni","sequence":"additional","affiliation":[{"name":"University of California-San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","unstructured":"Rajeev Alur Rastislav Bodik Garvit Juniwal Milo M. K. Martin Mukund Raghothaman Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2013. Syntax-guided synthesis. In 2013 Formal Methods in Computer-Aided Design. 1\u20138. https:\/\/doi.org\/10.1109\/FMCAD.2013.6679385 10.1109\/FMCAD.2013.6679385","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00501-3"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103677"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689747"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1093\/COMJNL\/12.1.41"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273442.1250743"},{"key":"e_1_2_1_7_1","series-title":"Series A, Mathematical and Physical Sciences, 312, 1522","volume-title":"The characterization problem for Hoare logics. Philosophical Transactions of the Royal Society of London","author":"Clarke Edmund M","year":"1984","unstructured":"Edmund M Clarke, Jr. 1984. The characterization problem for Hoare logics. Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences, 312, 1522 (1984), 423\u2013440."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/322108.322121"},{"key":"e_1_2_1_9_1","unstructured":"Thibault Dardinier and Peter M\u00fcller. 2023. Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version). arxiv:2301.10037."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2063239.2063245"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192382"},{"key":"e_1_2_1_12_1","volume-title":"Formal Verification of Self Modifying Code. In Int. Conf. for Young Computer Scientists.","author":"Gerth R.","year":"1991","unstructured":"R. Gerth. 1991. Formal Verification of Self Modifying Code. In Int. Conf. for Young Computer Scientists."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68863-1_8"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926423"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_18"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_21"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571216"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434311"},{"key":"e_1_2_1_20_1","unstructured":"Jinwoo Kim Shaan Nagy Thomas Reps and Loris D\u2019Antoni. 2024. Semantics of Sets of Programs. arxiv:2410.16102. arxiv:2410.16102"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/164793"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567082"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54572-7_6"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706313"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689715"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1090\/s0002-9939-1958-0135681-9"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45793-3_8"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814310"},{"key":"e_1_2_1_31_1","unstructured":"D. Schmidt. 1986. Denotational Semantics. Allyn and Bacon Inc. Boston MA. https:\/\/web.archive.org\/web\/20050308103715\/http:\/\/www.cis.ksu.edu\/~schmidt\/text\/densem.html"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/540155"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586045"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720515","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720515","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:12:58Z","timestamp":1760029978000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720515"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":35,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720515"],"URL":"https:\/\/doi.org\/10.1145\/3720515","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}