一句话：提出从语法与封闭解释器自动合成 CHC 形式语义的 CEGIS 算法，并实现 SynAntic 工具。
论文解决程序验证与合成框架中用户难以手写形式语义的问题。给定描述语言语法的文法和一个可执行的黑盒解释器，作者提出自动合成归纳定义的、语法导向的形式语义，并将其表示为约束 Horn 子句（CHC）。核心方法是反例引导合成（CEGIS），把合成一组 CHC 的难题拆成多个可由现有 SyGuS 合成器求解的小型表达式合成问题。工具 SynAntic 在 14 个程序合成应用所用语言的解释器上成功合成形式语义；还为某正则表达式语言发现解释器语义不一致，修复后提升语义效率，并使合成器在某些案例上加速 1.2 倍。
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 ( i ) a grammar describing the syntax of a language and ( ii ) 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 hard 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 SynAntic 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{LiuMGJRD24,
title = {Synthesizing Formal Semantics from Executable Interpreters},
author = {Jiangyi Liu and Charlie Murphy and Anvay Grover and Keith J.C. Johnson and Thomas Reps and Loris D’Antoni},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689724}
}