从多项式不变量到线性循环
From Polynomial Invariants to Linear Loops
AI总结：
针对软件验证中多项式不变量生成的难题，本文提出反向思路，利用代数几何技术从纯差分二项式描述的多项式不变量合成线性循环，并引入算法构造出构造上正确的线性循环。
摘要：
循环不变量是在循环的每次迭代前后均成立的软件属性。因此，不变量提供了归纳论证，是自动化验证程序循环的关键。生成循环不变量，特别是由多项式关系描述的不变量（即多项式不变量），是软件验证中最困难的问题之一。在本文中，我们提出了一种生成不变量的替代方案。我们不是从循环中推断不变量，而是从不变量合成循环。因此，我们生成的循环满足给定的一组多项式；换言之，我们合成的循环在构造上是正确的。我们的工作将循环合成问题转化为符号计算的挑战。我们采用代数几何技术来合成循环，其多项式不变量由纯差分二项式描述。我们证明这类复杂的多项式不变量“仅需”线性循环，为程序优化开辟了新途径。我们证明了对于由纯差分二项式生成的多项式不变量，存在具有线性更新的非平凡循环。重要的是，我们引入了一种算法方法，通过生成在其项之间具有特定代数关系的线性递归序列，从这类多项式不变量构造线性循环。
英文摘要：
Loop invariants are software properties that hold before and after every iteration of a loop. As such, invariants provide inductive arguments that are key in automating the verification of program loops. The problem of generating loop invariants; in particular, invariants described by polynomial relations (so called polynomial invariants), is therefore one of the hardest problems in software verification. In this paper we advocate an alternative solution to invariant generation. Rather than inferring invariants from loops, we synthesise loops from invariants. As such, we generate loops that satisfy a given set of polynomials; in other words, our synthesised loops are correct by construction. Our work turns the problem of loop synthesis into a symbolic computation challenge. We employ techniques from algebraic geometry to synthesise loops whose polynomial invariants are described by pure difference binomials. We show that such complex polynomial invariants need ``only'' linear loops, opening up new venues in program optimisation. We prove the existence of non-trivial loops with linear updates for polynomial invariants generated by pure difference binomials. Importantly, we introduce an algorithmic approach that constructs linear loops from such polynomial invariants, by generating linear recurrence sequences that have specified algebraic relations among their terms.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
