{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:28:17Z","timestamp":1784255297269,"version":"3.55.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"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":[[2023,1,9]]},"abstract":"<jats:p>\n                    We consider the problem of establishing that a program-synthesis problem is\n                    <jats:italic toggle=\"yes\">unrealizable<\/jats:italic>\n                    (i.e., has no solution in a given search space of programs). Prior work on unrealizability has developed some automatic techniques to establish that a problem is unrealizable; however, these techniques are all\n                    <jats:italic toggle=\"yes\">black-box<\/jats:italic>\n                    , meaning that they conceal the reasoning behind\n                    <jats:italic toggle=\"yes\">why<\/jats:italic>\n                    a synthesis problem is unrealizable.\n                  <\/jats:p>\n                  <jats:p>\n                    In this paper, we present a Hoare-style reasoning system, called\n                    <jats:italic toggle=\"yes\">unrealizability logic<\/jats:italic>\n                    for establishing that a program-synthesis problem is unrealizable. To the best of our knowledge, unrealizability logic is the first proof system for overapproximating the execution of an infinite set of imperative programs. The logic provides a general, logical system for building checkable proofs about unrealizability. Similar to how Hoare logic distills the fundamental concepts behind algorithms and tools to prove the correctness of programs, unrealizability logic distills into a single logical system the fundamental concepts that were hidden within prior tools capable of establishing that a program-synthesis problem is unrealizable.\n                  <\/jats:p>","DOI":"10.1145\/3571216","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T16:58:14Z","timestamp":1673456294000},"page":"659-688","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Unrealizability Logic"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3897-1828","authenticated-orcid":false,"given":"Jinwoo","family":"Kim","sequence":"first","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"},{"name":"Seoul National University, Seoul, Republic of Korea"}],"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 Wisconsin-Madison, Madison, 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"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00501-3"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.7"},{"key":"e_1_2_2_4_1","article-title":"On Undecidable Propositions of Formal Mathematical Systems. PostscriptumIntroductory Note to 1934","volume":"55","author":"Davis Martin","year":"1990","unstructured":"Martin Davis, Kurt Godel, and Stephen C Kleene. 1990. On Undecidable Propositions of Formal Mathematical Systems. PostscriptumIntroductory Note to 1934. Journal of Symbolic Logic, 55, 1 (1990).","journal-title":"Journal of Symbolic Logic"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_12"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523726"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192382"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_18"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385979"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_21"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_16"},{"key":"e_1_2_2_16_1","unstructured":"Jinwoo Kim Loris D\u2019Antoni and Thomas Reps. 2022. Unrealizability Logic. arXiv preprint arXiv:2211.07117."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434311"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-1793-7_2"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236049"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54572-7_6"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45793-3_8"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46691-6_13"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304059"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/151145"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571216","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571216","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T07:34:17Z","timestamp":1767944057000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571216"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":28,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571216"],"URL":"https:\/\/doi.org\/10.1145\/3571216","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2022-07-07","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-01-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}