{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:25:52Z","timestamp":1787592352589,"version":"build-2736575974"},"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\/legalcode"}],"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\u2014i.e., an inductively defined set of programs. Current verification frameworks overapproximate programs\u2019 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. Tracking this information is both necessary and sufficient for verification. We 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. We 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. Thus, 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_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00501-3"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103677"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689747"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1093\/COMJNL\/12.1.41"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/1273442.1250743"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.1984.0068"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/322108.322121"},{"key":"e_1_3_2_10_2","doi-asserted-by":"crossref","unstructured":"Thibault Dardinier and Peter M\u00fcller. 2023. Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version). arXiv:2301.10037 [cs.LO]","DOI":"10.1145\/3656437"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/2063239.2063245"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192382"},{"key":"e_1_3_2_13_2","unstructured":"R. Gerth. 1991. Formal Verification of Self Modifying Code. In Int. Conf. for Young Computer Scientists."},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Alexander Gruler Martin Leucker and Kathrin Scheidemann. 2008. Modeling and Model Checking Software Product Lines. In Proceedings of the 10th IFIPWG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (Oslo Norway) (FMOODS \u201908). Springer-Verlag Berlin Heidelberg 113\u2013131. https:\/\/doi.org\/10.1007\/978-3-540-68863-1_8 10.1007\/978-3-540-68863-1_8","DOI":"10.1007\/978-3-540-68863-1_8"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926423"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_18"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_21"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571216"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434311"},{"key":"e_1_3_2_21_2","unstructured":"Jinwoo Kim Shaan Nagy Thomas Reps and Loris D\u2019Antoni. 2024. Semantics of Sets of Programs. arXiv:2410.16102 [cs.PL] https:\/\/arxiv.org\/abs\/2410.16102"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.1"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/164793"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Zohar Manna and Amir Pnueli. 1983. How to Cook a Temporal Proof System for Your Pet Language. In Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages Austin Texas USA January 1983. 141\u2013154. https:\/\/doi.org\/10.1145\/567067.567082 10.1145\/567067.567082","DOI":"10.1145\/567067.567082"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54572-7_6"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Magnus O Myreen. 2010. Verified just-in-time compiler on x86. In Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 107\u2013118. https:\/\/doi.org\/10.1145\/1706299.1706313 10.1145\/1706299.1706313","DOI":"10.1145\/1706299.1706313"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689715"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1958-0135681-9"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45793-3_8"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Oleksandr Polozov and Sumit Gulwani. 2015. FlashMeta: a framework for inductive program synthesis. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming Systems Languages and Applications. 107\u2013126. https:\/\/doi.org\/10.1145\/2814270.2814310 10.1145\/2814270.2814310","DOI":"10.1145\/2814270.2814310"},{"key":"e_1_3_2_32_2","volume-title":"Denotational Semantics","year":"1986","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_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.5555\/540155"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","unstructured":"Emina Torlak and Rastislav Bod\u00edk. 2014. A lightweight symbolic virtual machine for solver-aided host languages. In ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI \u201914 Edinburgh United Kingdom - June 09 - 11 2014. 530\u2013541. https:\/\/doi.org\/10.1145\/2594291.2594340 10.1145\/2594291.2594340","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_3_2_36_2","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":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720515","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:31:24Z","timestamp":1787589084000},"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"}}]}}