Program synthesis using abstraction refinement
Program synthesis using abstraction refinement
复制标题
DOI：
10.1145/3158151
复制
发表时间：
2017-10
影响因子：
--
通讯作者：
Xinyu Wang;Işıl Dillig;Rishabh Singh
中科院分区：
文献类型：
--
作者：
Xinyu Wang;Işıl Dillig;Rishabh Singh
我们提出了一种新的方法，基于反例引导的抽象细化的例子引导的程序综合。我们的方法使用的抽象语义的底层DSL找到一个程序P的抽象行为满足的例子。然而，由于程序P可能是虚假的具体语义，我们的方法迭代地细化的抽象，直到我们找到一个程序，满足的例子或证明没有这样的DSL程序存在。由于许多程序在其抽象语义方面具有相同的输入-输出行为，因此与使用纯粹具体语义的现有技术相比，这种合成方法显着减少了搜索空间。虽然合成使用抽象细化（SYNGAR）可以在不同的设置中实现，我们提出了一个基于细化的合成算法，使用抽象有限树自动机（AFTA）。我们的技术使用一个粗略的初始程序抽象来构建一个初始的AFTA，这是迭代完善，通过构建任何虚假程序的不正确性证明。除了排除以前的AFTA所接受的虚假程序外，不正确性的证明也有助于排除许多其他虚假程序。我们实现这些想法在一个框架称为火焰，它可以在不同的领域提供一个合适的DSL和相应的具体和抽象的语义实例化。我们已经使用了Blaze框架来构建字符串和矩阵变换的合成器，并将Blaze与现有技术进行了比较。我们对字符串域的研究结果表明，Blaze与FlashFill相比毫不逊色，FlashFill是一个特定于域的合成器，现在部署在Microsoft PowerShell中。在矩阵操作的背景下，我们比较了火焰对散文，一个国家的最先进的通用VSA为基础的合成器，并表明火焰的结果在一个90倍的速度超过散文。在这两个应用领域中，Blaze还持续地将其他两种现有技术的性能提高了至少一个数量级。
We present a new approach to example-guided program synthesis based on counterexample-guided abstraction refinement. Our method uses the abstract semantics of the underlying DSL to find a program P whose abstract behavior satisfies the examples. However, since program P may be spurious with respect to the concrete semantics, our approach iteratively refines the abstraction until we either find a program that satisfies the examples or prove that no such DSL program exists. Because many programs have the same input-output behavior in terms of their abstract semantics, this synthesis methodology significantly reduces the search space compared to existing techniques that use purely concrete semantics. While synthesis using abstraction refinement (SYNGAR) could be implemented in different settings, we propose a refinement-based synthesis algorithm that uses abstract finite tree automata (AFTA). Our technique uses a coarse initial program abstraction to construct an initial AFTA, which is iteratively refined by constructing a proof of incorrectness of any spurious program. In addition to ruling out the spurious program accepted by the previous AFTA, proofs of incorrectness are also useful for ruling out many other spurious programs. We implement these ideas in a framework called Blaze, which can be instantiated in different domains by providing a suitable DSL and its corresponding concrete and abstract semantics. We have used the Blaze framework to build synthesizers for string and matrix transformations, and we compare Blaze with existing techniques. Our results for the string domain show that Blaze compares favorably with FlashFill, a domain-specific synthesizer that is now deployed in Microsoft PowerShell. In the context of matrix manipulations, we compare Blaze against Prose, a state-of-the-art general-purpose VSA-based synthesizer, and show that Blaze results in a 90x speed-up over Prose. In both application domains, Blaze also consistently improves upon the performance of two other existing techniques by at least an order of magnitude.