迭代前向-后向抽象解释的归纳程序合成
摘要：基于示例的程序合成面临的主要挑战是庞大的程序搜索空间。为了解决这个挑战，已经提出了各种使用抽象解释来剪枝搜索空间的方法。然而，大部分现有方法仅关注前向抽象解释，因此不能充分发挥抽象解释的威力。在本文中，我们提出了一种通过迭代前向-后向抽象解释进行归纳程序合成的新方法。前向抽象解释计算给定输入的程序可能的输出，而后向抽象解释计算给定输出的程序可能的输入。通过交替进行这两种抽象解释的迭代，我们可以有效确定每个部分程序的任何补全是否能够满足输入-输出示例。我们将我们的方法应用于标准的语法引导合成（SyGuS）问题，从而支持广泛的归纳合成任务。我们已经实现了我们的方法，并在一组来自之前工作的基准测试中进行了评估。实验结果表明，由于高级抽象解释技术，我们的方法显著优于现有技术。
作者：Yongho Yoon, Woosuk Lee, Kwangkeun Yi
论文ID：2304.10768
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-04-24