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.

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