基于模板的非线性不变综合的广义齐次多项式
Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis
摘要：
基于模板的方法是代数不变量综合中最成功的方法之一。在该方法中，算法指定程序变量上的模板多项式p，生成p=0的约束为不变量，并求解生成的约束。然而，如果模板多项式的次数太高，则这种方法经常遭受增加的模板大小。我们提出了一种技术，使基于模板的方法更有效。我们的技术是基于以下发现：如果一个代数不变存在，那么有一个特定的代数不变，我们称之为广义齐次代数不变，往往是较小的。这一发现证明只使用一个较小的模板，对应于一个广义齐次代数不变。具体地说，我们正式声明我们的发现上面提出的一个命令式程序的抽象语义的基础上，由Cachera等人。然后，我们修改他们的基于模板的不变式合成，使它只生成广义齐次代数不变量。实践证明，这种修改是合理的。此外，我们还实证证明了限制广义齐次代数不变量的优点。我们的实现优于Cachera等人。对于需要更高程度模板的程序。
英文摘要：
The template-based method is one of the most successful approaches to algebraic invariant synthesis. In this method, an algorithm designates a template polynomial p over program variables, generates constraints for p=0 to be an invariant, and solves the generated constraints. However, this approach often suffers from an increasing template size if the degree of a template polynomial is too high. We propose a technique to make template-based methods more efficient. Our technique is based on the following finding: If an algebraic invariant exists, then there is a specific algebraic invariant that we call a generalized homogeneous algebraic invariant that is often smaller. This finding justifies using only a smaller template that corresponds to a generalized homogeneous algebraic invariant. Concretely, we state our finding above formally based on the abstract semantics of an imperative program proposed by Cachera et al. Then, we modify their template-based invariant synthesis so that it generates only generalized homogeneous algebraic invariants. This modification is proved to be sound. Furthermore, we also empirically demonstrate the merit of the restriction to generalized homogeneous algebraic invariants. Our implementation outperforms that of Cachera et al. for programs that require a higher-degree template.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
