Bottom-up synthesis of recursive functional programs using angelic execution
Bottom-up synthesis of recursive functional programs using angelic execution
复制标题
使用天使执行的递归函数程序的自下而上综合
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Işıl Dillig
中科院分区：
文献类型：
--
作者：
Anders Miltner;A. Nunez;Ana Brendel;Swarat Chaudhuri;Işıl Dillig
提出了一种新的自底向上的函数递归程序综合方法。虽然自底向上的合成技术在某些情况下比自顶向下的方法工作得更好，但没有一种技术可以以纯粹的自底向上的方式从逻辑规范合成递归程序。主要的挑战是，有效的自底向上方法需要执行正在合成的代码的子表达式，但不可能执行尚未完全构造的程序的递归子表达式。在本文中，我们使用天使语义的概念来解决这一挑战。具体来说，我们的方法找到一个程序，满足规范下天使的语义（我们称之为天使合成），分析其天使执行过程中所作的假设，使用这种分析，以加强规范，并最终重新尝试合成与加强规范。我们提出的天使合成算法是基于版本空间学习，因此有效地处理许多增量合成调用整个算法。我们已经实现了这种方法在一个原型称为突发和评估它的合成问题，从以前的工作。我们的实验表明，突发是能够合成的解决方案，94%的基准在我们的基准套件，优于以前的工作。
We present a novel bottom-up method for the synthesis of functional recursive programs. While bottom-up synthesis techniques can work better than top-down methods in certain settings, there is no prior technique for synthesizing recursive programs from logical specifications in a purely bottom-up fashion. The main challenge is that effective bottom-up methods need to execute sub-expressions of the code being synthesized, but it is impossible to execute a recursive subexpression of a program that has not been fully constructed yet. In this paper, we address this challenge using the concept of angelic semantics. Specifically, our method finds a program that satisfies the specification under angelic semantics (we refer to this as angelic synthesis), analyzes the assumptions made during its angelic execution, uses this analysis to strengthen the specification, and finally reattempts synthesis with the strengthened specification. Our proposed angelic synthesis algorithm is based on version space learning and therefore deals effectively with many incremental synthesis calls made during the overall algorithm. We have implemented this approach in a prototype called Burst and evaluate it on synthesis problems from prior work. Our experiments show that Burst is able to synthesize a solution to 94% of the benchmarks in our benchmark suite, outperforming prior work.
DOI：
10.1145/3385412.3386027
发表时间：
2020
期刊：
Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Huang, Kangjing;Qiu, Xiaokang;Shen, Peiyuan;Wang, Yanjun
通讯作者：
Wang, Yanjun
循环程序综合
DOI：
10.1145/3453483.3454087
发表时间：
2021
期刊：
Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Itzhaky, Shachar;Peleg, Hila;Polikarpova, Nadia;Rowe, Reuben N.;Sergey, Ilya
通讯作者：
Sergey, Ilya
通过实时双向评估进行程序草图绘制
影响因子：
--
作者：
Lubin, Justin;Collins, Nick;Omar, Cyrus;Chugh, Ravi
通讯作者：
Chugh, Ravi