{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:05:08Z","timestamp":1784199908964,"version":"3.55.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T00:00:00Z","timestamp":1749772800000},"content-version":"vor","delay-in-days":3,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n                    Semantics-Guided Synthesis (SemGuS) provides a framework to specify synthesis problems in a solver-agnostic and domain-agnostic way, by allowing a user to provide both the syntax and semantics of the language in which the desired program should be synthesized. Because synthesis and verification are closely intertwined, the SemGuS framework raises the following question:\n                    <jats:italic toggle=\"yes\">how does one verify that a user-given program satisfies a given specification when interpreted according to a user-given semantics?<\/jats:italic>\n                  <\/jats:p>\n                  <jats:p>\n                    In this paper, we prove that this form of\n                    <jats:italic toggle=\"yes\">language-agnostic<\/jats:italic>\n                    verification (specifically that verifying whether a program is a valid solution to a SemGuS problem) can be reduced to proving validity of a query in the \ud835\udf07CLP calculus, a fixed-point logic that is capable of expressing alternating least and greatest fixed-points. Our encoding into \ud835\udf07CLP allows us to further classify the SemGuS verification problems into ones that are reducible to satisfiability of (\n                    <jats:italic toggle=\"yes\">i<\/jats:italic>\n                    ) first-order-logic formulas, (\n                    <jats:italic toggle=\"yes\">ii<\/jats:italic>\n                    ) Constrained Horn Clauses, and (\n                    <jats:italic toggle=\"yes\">iii<\/jats:italic>\n                    ) \ud835\udf07CLP queries. Furthermore, our encoding shines light on some limitations of the SemGuS framework, such as its inability to model nondeterminism and reactive synthesis. We thus propose a modification to SemGuS that makes it more expressive, and for which verifying solutions is exactly equivalent to proving validity of a query in the \ud835\udf07CLP calculus. Our implementation of SemGuS verifiers based on the above encoding can verify instances that were not even encodable in previous work. Furthermore, we use our SemGuS verifiers within an enumeration-based SemGuS solver to correctly synthesize solutions to SemGuS problems that no previous SemGuS synthesizer could solve.\n                  <\/jats:p>","DOI":"10.1145\/3729320","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1741-1765","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Verifying Solutions to Semantics-Guided Synthesis Problems"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4813-7578","authenticated-orcid":false,"given":"Charlie","family":"Murphy","sequence":"first","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3766-5204","authenticated-orcid":false,"given":"Keith J.C.","family":"Johnson","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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9625-4037","authenticated-orcid":false,"given":"Loris","family":"D'Antoni","sequence":"additional","affiliation":[{"name":"University of California at San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96415-3_15"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Marco Albertini Davide Davalos Paolo Tortori Marco Gavagnin Evelina Lamma and Paola Mello. 2004. Specification and verification of agent interaction protocols in a logic-based system. In Proceedings of the ACM Symposium on Applied Computing 72-78. https:\/\/doi.org\/10.1145\/967900.967918 10.1145\/967900.967918","DOI":"10.1145\/967900.967918"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2018.02.021"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56610-4_60"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/2237796.2237811"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.29007\/vv21"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_27"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-86205-3_1"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39666-3_5"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_4"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158149"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.234.7"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC.2012.69"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC49474.2019.00010"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_24"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.24042\/EPCTCS344.5"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65633-0_2"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434311"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0326-7"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_59"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3586029"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_49"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Charlie Murphy Keith Johnson Thomas Reps and Loris D\u2019Antoni. 2024. Verifying Solutions to Semantics-Guided Synthesis Problems. https:\/\/doi.org\/10.48550\/arXiv.2408.15475 10.48550\/arXiv.2408.15475 arXiv:2408.15475 [cs.PL]","DOI":"10.48550\/arXiv.2408.15475"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_31"},{"key":"e_1_3_2_36_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-126. https:\/\/doi.org\/10.1145\/2858965.2814310 10.1145\/2858965.2814310","DOI":"10.1145\/2858965.2814310"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Vasumathi Raman Alexandre Donz\u00e9 Dorsa Sadigh Richard M Murray and Sanjit A Seshia. 2015. Reactive synthesis from signal temporal logic specifications. In Proceedings of the 18th international conference on hybrid systems: computation and control 239-248. https:\/\/doi.org\/10.1145\/2728606.2728628 10.1145\/2728606.2728628","DOI":"10.1145\/2728606.2728628"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3022677.2984027"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158100"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571265"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_35"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932500"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0263-6"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729320","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729320","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:05:49Z","timestamp":1784196349000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729320"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":42,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729320"],"URL":"https:\/\/doi.org\/10.1145\/3729320","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}