Reconciling enumerative and deductive program synthesis
Reconciling enumerative and deductive program synthesis
复制标题
协调枚举和演绎程序综合
DOI：
10.1145/3385412.3386027
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Wang, Yanjun
中科院分区：
文献类型：
--
作者：
Huang, Kangjing;Qiu, Xiaokang;Shen, Peiyuan;Wang, Yanjun
语法引导的综合（SyGuS）的目的是找到一个程序满足语义规范以及用户提供的结构假设。有两种主要的合成方法：枚举合成，它重复枚举可能的候选程序并检查它们的正确性，以及演绎合成，它利用符号过程来构建规范的实现。两种方法严格来说都不优于另一种：自动演绎合成通常非常有效，但只适用于特殊的语法或应用程序;枚举综合是一种非常普遍的方法，但在可扩展性方面受到限制.本文提出了一种基于条件线性整数运算（CLIA）背景理论的SyGuS问题的协同综合技术，作为这两种方法的一种新的集成，结合了两个世界的精华该技术利用了几种新颖的分治策略，将一个大的综合问题分解为较小的子问题。这些子问题被分别求解，它们的解被合并形成最终解。该技术集成了两个合成引擎：一个是可以有效解决某些问题的纯演绎组件，另一个是可以处理任意语法的基于高度的枚举算法。我们实现了合作合成技术，并评估了广泛的基准。实验表明，我们的技术可以解决许多具有挑战性的合成问题之前不可能的，往往是更可扩展性比国家的最先进的合成算法。
Syntax-guided synthesis (SyGuS) aims to find a program satisfying semantic specification as well as user-provided structural hypotheses. There are two main synthesis approaches: enumerative synthesis, which repeatedly enumerates possible candidate programs and checks their correctness, and deductive synthesis, which leverages a symbolic procedure to construct implementations from specifications. Neither approach is strictly better than the other: automated deductive synthesis is usually very efficient but only works for special grammars or applications; enumerative synthesis is very generally applicable but limited in scalability.In this paper, we propose a cooperative synthesis technique for SyGuS problems with the conditional linear integer arithmetic (CLIA) background theory, as a novel integration of the two approaches, combining the best of the two worlds. The technique exploits several novel divide-and-conquer strategies to split a large synthesis problem to smaller subproblems. The subproblems are solved separately and their solutions are combined to form a final solution. The technique integrates two synthesis engines: a pure deductive component that can efficiently solve some problems, and a height-based enumeration algorithm that can handle arbitrary grammar. We implemented the cooperative synthesis technique, and evaluated it on a wide range of benchmarks. Experiments showed that our technique can solve many challenging synthesis problems not possible before, and tends to be more scalable than state-of-the-art synthesis algorithms.
登录
查看更多内容
影响因子：
0.8
作者：
Jinseong Jeon;Xiaokang Qiu;Armando Solar;J. Foster
通讯作者：
J. Foster
并行程序综合的自适应具体化
DOI：
10.1007/978-3-319-21668-3_22
发表时间：
2015
期刊：
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Jinseong Jeon;Xiaokang Qiu;Armando Solar;J. Foster
通讯作者：
J. Foster
SyGuS-Comp15 的结果和分析
影响因子：
1.6
作者：
R. Alur;D. Fisman;Rishabh Singh;Armando Solar
通讯作者：
Armando Solar
影响因子：
--
作者：
Yu Feng;R. Martins;O. Bastani;Işıl Dillig
通讯作者：
Yu Feng;R. Martins;O. Bastani;Işıl Dillig
综合：梦想 - 程序
DOI：
10.1109/tse.1979.234198
发表时间：
1979
期刊：
IEEE Trans. Software Eng.
影响因子：
--
作者：
Z. Manna;R. Waldinger
通讯作者：
R. Waldinger