{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T21:57:30Z","timestamp":1770242250066,"version":"3.49.0"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"<jats:p>\n                    Automated verification of all members of a (potentially infinite) set of programs has the potential to be useful in program synthesis, as well as in verification of dynamically loaded code, concurrent code, and language properties. Existing techniques for verification of sets of programs are limited in scope and unable to create or use interpretable or reusable information about sets of programs. The consequence is that one cannot learn anything from one verification problem that can be used in another. Unrealizability Logic (UL), proposed by Kim et al. as the first Hoare-style proof system to prove properties over sets of programs (defined by a regular tree grammar), presents a theoretical framework that can express and use reusable insight. In particular, UL features\n                    <jats:italic toggle=\"yes\">nonterminal summaries<\/jats:italic>\n                    \u2014inductive facts that characterize recursive nonterminals (analogous to procedure summaries in Hoare logic). In this work, we design the first UL proof synthesis algorithm, implemented as\n                    <jats:sc>Wuldo<\/jats:sc>\n                    . Specifically, we decouple the problem of deciding how to apply UL rules from the problem of synthesizing\/checking nonterminal summaries by computing proof structure in a fully syntax-directed fashion. We show that\n                    <jats:sc>Wuldo<\/jats:sc>\n                    , when provided nonterminal summaries, can express and prove verification problems beyond the reach of existing tools, including establishing how infinitely many programs behave on infinitely many inputs. In some cases,\n                    <jats:sc>Wuldo<\/jats:sc>\n                    can even synthesize the necessary nonterminal summaries. Moreover,\n                    <jats:sc>Wuldo<\/jats:sc>\n                    can reuse previously proven nonterminal summaries across verification queries, making verification 1.96 times as fast as when summaries are instead proven from scratch.\n                  <\/jats:p>","DOI":"10.1145\/3689715","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"113-139","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8015-5421","authenticated-orcid":false,"given":"Shaan","family":"Nagy","sequence":"first","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3897-1828","authenticated-orcid":false,"given":"Jinwoo","family":"Kim","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, South Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"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":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9625-4037","authenticated-orcid":false,"given":"Loris","family":"D\u2019Antoni","sequence":"additional","affiliation":[{"name":"University of California San Diego, San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_1_3_2","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2\u20137, 2022, Proceedings, Part I","author":"Barbosa Haniel","year":"2022","unstructured":"Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres N\u00f6tzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. Cvc5: A Versatile and Industrial-Strength SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2\u20137, 2022, Proceedings, Part I (Munich, Germany). Springer-Verlag, Berlin, Heidelberg, 415\u2013442. https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24 10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_1_4_2","first-page":"173","volume-title":"International Conference on Logic for Programming Artificial Intelligence and Reasoning","author":"Blanc R\u00e9gis","year":"2013","unstructured":"R\u00e9gis Blanc, Ashutosh Gupta, Laura Kov\u00e1cs, and Bernhard Kragl. 2013. Tree interpolation in vampire. In International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer, 173\u2013181. https:\/\/doi.org\/10.1007\/978-3-642-45221-5_1310.1007\/978-3-642-45221-5_13"},{"issue":"6","key":"e_1_3_1_5_2","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1145\/1273442.1250743","article-title":"Certified self-modifying code","volume":"42","author":"Cai Hongxu","year":"2007","unstructured":"Hongxu Cai, Zhong Shao, and Alexander Vaynberg. 2007. Certified self-modifying code. SIGPLAN Not. 42, 6 (jun 2007), 66\u201377. https:\/\/doi.org\/10.1145\/1273442.1250743 10.1145\/1273442.1250743","journal-title":"SIGPLAN Not"},{"key":"e_1_3_1_6_2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-031-44245-2_1","volume-title":"Static Analysis","author":"D\u2019Antoni Loris","year":"2023","unstructured":"Loris D\u2019Antoni. 2023. Verifying Infinitely Many Programs at Once. In Static Analysis, Manuel V. Hermenegildo and Jos\u00e9 F. Morales (Eds.). Springer Nature Switzerland, Cham, 3\u20139. https:\/\/doi.org\/10.1007\/978-3-031-44245-2_1 10.1007\/978-3-031-44245-2_1"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_3_1_8_2","first-page":"244","article-title":"Recursion synthesis with unrealizability witnesses","author":"Farzan Azadeh","year":"2022","unstructured":"Azadeh Farzan, Danya Lette, and Victor Nicolet. 2022. Recursion synthesis with unrealizability witnesses. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 244\u2013259. https:\/\/doi.org\/10.1145\/3519939.3523726 10.1145\/3519939.3523726","journal-title":"Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation"},{"key":"e_1_3_1_9_2","volume-title":"International Conference on Computer Aided Verification","author":"Garg Pranav","year":"2014","unstructured":"Pranav Garg, Christof L\u00f6ding, P. Madhusudan, and Daniel Neider. 2014. ICE: A Robust Framework for Learning Invariants. In International Conference on Computer Aided Verification. Springer-Verlag, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-319-08867-9_5 10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_3_1_11_2","unstructured":"Sankha Narayan Guria. 2023. Program Synthesis with Lightweight Abstractions. Ph.D. Dissertation. University of Maryland College Park. https:\/\/doi.org\/10.13016\/dspace\/txaj-5df6 10.13016\/dspace\/txaj-5df6"},{"key":"e_1_3_1_12_2","first-page":"102","volume-title":"Symposium on semantics of algorithmic languages","author":"Richard Hoare Charles Antony","year":"2006","unstructured":"Charles Antony Richard Hoare. 2006. Procedures and parameters: An axiomatic approach. In Symposium on semantics of algorithmic languages. Springer, 102\u2013116. https:\/\/doi.org\/10.5555\/63445.C1104361 10.5555\/63445.C1104361"},{"key":"e_1_3_1_13_2","first-page":"335","volume-title":"International Conference on Computer Aided Verification","author":"Qinheping Hu","year":"2019","unstructured":"Qinheping Hu, Jason Breck, John Cyphert, Loris D\u2019Antoni, and Thomas Reps. 2019. Proving unrealizability for syntax-guided synthesis. In International Conference on Computer Aided Verification. Springer, 335\u2013352. https:\/\/doi.org\/10.1007\/978-3-030-25540-4_18 10.1007\/978-3-030-25540-4_18"},{"key":"e_1_3_1_14_2","doi-asserted-by":"crossref","unstructured":"Qinheping Hu John Cyphert Loris D\u2019Antoni and Thomas Reps. 2020. Exact and approximate methods for proving unrealizability of syntax-guided synthesis problems. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. 1128\u20131142. https:\/\/doi.org\/10.1145\/3385412.3385979 10.1145\/3385412.3385979","DOI":"10.1145\/3385412.3385979"},{"key":"e_1_3_1_15_2","first-page":"386","volume-title":"International Conference on Computer Aided Verification","author":"Qinheping Hu","year":"2018","unstructured":"Qinheping Hu and Loris D\u2019Antoni. 2018. Syntax-guided synthesis with quantitative syntactic objectives. In International Conference on Computer Aided Verification. Springer, 386\u2013403. https:\/\/doi.org\/10.1007\/978-3-319-96145-3_21 10.1007\/978-3-319-96145-3_21"},{"key":"e_1_3_1_16_2","doi-asserted-by":"crossref","unstructured":"Marius Kamp and Michael Philippsen. 2021. Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible. In Verification Model Checking and Abstract Interpretation - 22nd International Conference VMCAI 2021 Copenhagen Denmark January 17-19 2021 Proceedings (Lecture Notes in Computer Science Vol. 12597) Fritz Henglein Sharon Shoham and Yakir Vizel (Eds.). Springer 353\u2013375. https:\/\/doi.org\/10.1007\/978-3-030-67067-2_16 10.1007\/978-3-030-67067-2_16","DOI":"10.1007\/978-3-030-67067-2_16"},{"key":"e_1_3_1_17_2","doi-asserted-by":"crossref","unstructured":"Jinwoo Kim Loris D'Antoni and Thomas Reps. 2023. Unrealizability logic. Proceedings of the ACM on Programming Languages 7 POPL (2023) 659\u2013688. https:\/\/doi.org\/10.1145\/3571216 10.1145\/3571216","DOI":"10.1145\/3571216"},{"key":"e_1_3_1_18_2","first-page":"1","article-title":"Semantics-guided synthesis","author":"Kim Jinwoo","year":"2021","unstructured":"Jinwoo Kim, Qinheping Hu, Loris D'Antoni, and Thomas Reps. 2021. Semantics-guided synthesis. Proceedings of the ACM on Programming Languages 5, POPL (2021), 1\u201332. https:\/\/doi.org\/10.1145\/3434311 10.1145\/3434311","journal-title":"Proceedings of the ACM on Programming Languages 5"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192410"},{"key":"e_1_3_1_20_2","doi-asserted-by":"crossref","unstructured":"Sergey Mechtaev Alberto Griggio Alessandro Cimatti and Abhik Roychoudhury. 2018. Symbolic execution with existential second-order constraints. In Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 389\u2013399. https:\/\/doi.org\/10.1145\/3236024.3236049 10.1145\/3236024.3236049","DOI":"10.1145\/3236024.3236049"},{"key":"e_1_3_1_21_2","unstructured":"Shaan Nagy Jinwoo Kim Loris D'Antoni and Thomas Reps. 2024. Automating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of Programs. https:\/\/doi.org\/10.48550\/arXiv.2401.13244 10.48550\/arXiv.2401.13244 arXiv:2401.13244[cs.PL]"},{"key":"e_1_3_1_22_2","unstructured":"Shaan Nagy Jinwoo Kim Thomas Reps and Loris D\u2019Antoni. 2024. Wuldo Unrealizability Logic Proof Synthesizer. https:\/\/doi.org\/10.5281\/zenodo.12627576 10.5281\/zenodo.12627576"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90009-9"},{"key":"e_1_3_1_24_2","first-page":"364","volume-title":"Static Analysis","author":"So Sunbeom","year":"2017","unstructured":"Sunbeom So and Hakjoo Oh. 2017. Synthesizing Imperative Programs from Examples Guided by Static Analysis. In Static Analysis, Francesco Ranzato (Ed.). Springer International Publishing, Cham, 364\u2013381. https:\/\/doi.org\/10.1007\/978-3-319-66706-5_18 10.1007\/978-3-319-66706-5_18"},{"key":"e_1_3_1_25_2","unstructured":"Unrealizability Logic Corrigendum [n. d.]. Pending."},{"key":"e_1_3_1_26_2","unstructured":"Lu Zhengyang. 2023. Z3-Alpha: A Reinforcement Learning Guided Smt Solver. https:\/\/smt-comp.github.io\/2023\/system-descriptions\/z3-alpha.pdf"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689715","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689715","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:14:41Z","timestamp":1770196481000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689715"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":25,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689715"],"URL":"https:\/\/doi.org\/10.1145\/3689715","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-04","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}