论文标题
基于代数的循环合成
Algebra-based Loop Synthesis
论文作者
论文摘要
我们提出了一种用于满足给定多项式循环不变的综合程序循环的算法。我们认为的循环类别可以通过具有恒定系数的代数复发方程系统进行建模。通过精确表征满足给定不变的所有循环的集合，我们将循环合成的任务转变为多项式约束问题。我们证明了方法的合理性，以及与程序变量数量的先验固定上限相对于其完整性。我们的工作在程序验证中有应用，并从代数关系中生成数字序列。我们在Absynth工具中实施了工作，并报告了我们的最初循环合成实验。
We present an algorithm for synthesizing program loops satisfying a given polynomial loop invariant. The class of loops we consider can be modeled by a system of algebraic recurrence equations with constant coefficients. We turn the task of loop synthesis into a polynomial constraint problem by precisely characterizing the set of all loops satisfying the given invariant. We prove soundness of our approach, as well as its completeness with respect to an a priori fixed upper bound on the number of program variables. Our work has applications towards program verification, as well as generating number sequences from algebraic relations. We implemented our work in the Absynth tool and report on our initial experiments with loop synthesis.
