{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T00:39:24Z","timestamp":1790987964805,"version":"4.1.0"},"reference-count":21,"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\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1750965, CCF-1918211, CCF-2023222, CCF-2211968, CCF-2212558"],"award-info":[{"award-number":["CCF-1750965, CCF-1918211, CCF-2023222, CCF-2211968, CCF-2212558"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"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                    Program verification and synthesis frameworks that allow one to customize the language in which one is interested typically require the user to provide a formally defined semantics for the language. Because writing a formal semantics can be a daunting and error-prone task, this requirement stands in the way of such frameworks being adopted by non-expert users. We present an algorithm that can automatically synthesize inductively defined syntax-directed semantics when given (\n                    <jats:italic toggle=\"yes\">i<\/jats:italic>\n                    ) a grammar describing the syntax of a language and (\n                    <jats:italic toggle=\"yes\">ii<\/jats:italic>\n                    ) an executable (closed-box) interpreter for computing the semantics of programs in the language of the grammar. Our algorithm synthesizes the semantics in the form of Constrained-Horn Clauses (CHCs), a natural, extensible, and formal logical framework for specifying inductively defined relations that has recently received widespread adoption in program verification and synthesis. The key innovation of our synthesis algorithm is a Counterexample-Guided Synthesis (CEGIS) approach that breaks the\n                    <jats:italic toggle=\"yes\">hard<\/jats:italic>\n                    problem of synthesizing a set of constrained Horn clauses into small, tractable expression-synthesis problems that can be dispatched to existing SyGuS synthesizers. Our tool\n                    <jats:sc>SynAntic<\/jats:sc>\n                    synthesized inductively-defined formal semantics from 14 interpreters for languages used in program-synthesis applications. When synthesizing formal semantics for one of our benchmarks, Synantic unveiled an inconsistency in the semantics computed by the interpreter for a language of regular expressions; fixing the inconsistency resulted in a more efficient semantics and, for some cases, in a 1.2 x speedup for a synthesizer solving synthesis problems over such a language.\n                  <\/jats:p>","DOI":"10.1145\/3689724","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"362-388","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Synthesizing Formal Semantics from Executable Interpreters"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6525-4659","authenticated-orcid":false,"given":"Jiangyi","family":"Liu","sequence":"first","affiliation":[{"name":"University of Wisconsin - Madison, Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4813-7578","authenticated-orcid":false,"given":"Charlie","family":"Murphy","sequence":"additional","affiliation":[{"name":"University of Wisconsin - Madison, Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-4820-3560","authenticated-orcid":false,"given":"Anvay","family":"Grover","sequence":"additional","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\u2019Antoni","sequence":"additional","affiliation":[{"name":"University of California, San Diego, La Jolla, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66158-2_44"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_1_6_2","doi-asserted-by":"crossref","unstructured":"Xiaohong Chen and Grigore Rosu. 2019. A Semantic Framework for Programming Languages and Formal Analysis. In Engineering Trustworthy Software Systems - 5th International School SETSS 2019 Chongqing China April 21-27 2019 Tutorial Lectures (Lecture Notes in Computer Science Vol. 12154) Jonathan P. Bowen Zhiming Liu and Zili Zhang (Eds.). Springer 122\u2013158. https:\/\/doi.org\/10.1007\/978-3-030-55089-9_4 10.1007\/978-3-030-55089-9_4","DOI":"10.1007\/978-3-030-55089-9_4"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_4"},{"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.","journal-title":"Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_39"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-22308-2_13"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65633-0_2"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78971"},{"key":"e_1_3_1_13_2","first-page":"304","volume-title":"2022 Formal Methods in Computer-Aided Design (FMCAD)","author":"Kalita Pankaj Kumar","year":"2022","unstructured":"Pankaj Kumar Kalita, Miriyala Jeevan Kumar, and Subhajit Roy. 2022. Synthesis of semantic actions in attribute grammars. In 2022 Formal Methods in Computer-Aided Design (FMCAD). IEEE, 304\u2013314."},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434311"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571263"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/2450136.2450139"},{"key":"e_1_3_1_17_2","unstructured":"Jiangyi Liu Charlie Murphy Anvay Grover Keith Johnson Thomas Reps and Loris D'Antoni. 2024. Artifact of paper \u201cSynthesizing Formal Semantics from Executable Interpreters\u201d. https:\/\/doi.org\/10.5281\/zenodo.13368062 10.5281\/zenodo.13368062"},{"key":"e_1_3_1_18_2","unstructured":"Jiangyi Liu Charlie Murphy Anvay Grover Keith J. C. Johnson Thomas Reps and Loris D'Antoni. 2024. Synthesizing Formal Semantics from Executable Interpreters. arXiv:2408.14668 [cs.PL] https:\/\/arxiv.org\/abs\/2408.14668"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82627-1"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498682"},{"key":"e_1_3_1_21_2","unstructured":"Charlie Murphy Keith J. C. Johnson Thomas Reps and Loris D'Antoni. 2024. Verifying Solutions to Semantics-Guided Synthesis Problems. arXiv:2408.15475 [cs.PL] https:\/\/arxiv.org\/abs\/2408.15475"},{"key":"e_1_3_1_22_2","first-page":"515","article-title":"Syntax-guided synthesis of datalog programs","author":"Si Xujie","year":"2018","unstructured":"Xujie Si, Woosuk Lee, Richard Zhang, Aws Albarghouthi, Paraschos Koutris, and Mayur Naik. 2018. Syntax-guided synthesis of datalog programs. In Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 515\u2013527.","journal-title":"Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689724","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689724","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:03:27Z","timestamp":1770195807000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689724"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":21,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689724"],"URL":"https:\/\/doi.org\/10.1145\/3689724","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-06","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"}}]}}