一句话：提出 SemGuS 框架，允许以递归大步步语义定义合成问题，并用 CHC 证明搜索同时合成程序与证明不可实现性。
现有程序合成框架多依赖固定语法与标准语义，难以处理带无界循环的命令式语言或非标准、抽象语义下的合成问题。本文提出 SemGuS（语义引导合成）框架，用户可为语言构造同时提供语法和递归定义的大步步语义，从而支持命令式程序、抽象语义等合成问题。作者将 SemGuS 问题编码为约束 Horn 子句（CHC）上的证明搜索，既能合成程序，也能证明不可实现性；这是首个能在无限语法搜索空间上对带无界循环的命令式合成问题证明不可实现性的方法。实现工具 MESSY，并应用于 SyGuS（表达式）、命令式程序合成和正则表达式合成。
This paper develops a new framework for program synthesis, called semantics-guided synthesis (SemGuS), that allows a user to provide both the syntax and the semantics for the constructs in the language. SemGuS accepts a recursively defined big-step semantics, which allows it, for example, to be used to specify and solve synthesis problems over an imperative programming language that may contain loops with unbounded behavior. The customizable nature of SemGuS also allows synthesis problems to be defined over a non-standard semantics, such as an abstract semantics. In addition to the SemGuS framework, we develop an algorithm for solving SemGuS problems that is capable of both synthesizing programs and proving unrealizability, by encoding a SemGuS problem as a proof search over Constrained Horn Clauses: in particular, our approach is the first that we are aware of that can prove unrealizabilty for synthesis problems that involve imperative programs with unbounded loops, over an infinite syntactic search space. We implemented the technique in a tool called MESSY, and applied it to SyGuS problems (i.e., over expressions), synthesis problems over an imperative programming language, and synthesis problems over regular expressions.
@article{paperbot1182,
title = {Semantics-guided synthesis},
author = {Jinwoo Kim and Qinheping Hu and Loris D'Antoni and Thomas Reps},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434311}
}