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.

翻译：循环不变量是在循环的每一次迭代前后都成立的软件属性。因此，不变量提供了归纳论证，对于自动化验证程序循环至关重要。生成循环不变量，特别是由多项式关系描述的不变量（即所谓的多项式不变量），是软件验证中最困难的问题之一。本文提出了一种替代性的不变量生成方案，即不通过循环推断不变量，而是从不变量中合成循环。为此，我们生成满足给定多项式集的循环；换言之，我们合成的循环在构造上就是正确的。我们的工作将循环合成问题转化为符号计算挑战。我们采用代数几何技术来合成其多项式不变量由纯差分二元式描述的循环。我们证明，这类复杂的多项式不变量“仅需”线性循环，从而为程序优化开辟了新途径。我们证明，对于由纯差分二元式生成的多项式不变量，存在具有线性更新的非平凡循环。重要的是，我们引入了一种算法方法，通过生成各项之间具有指定代数关系的线性递推序列，从这类多项式不变量构造出线性循环。