Automatic generation of loop invariants is a fundamental challenge in software verification. While this task is undecidable in general, it is decidable for certain restricted classes of programs. This work focuses on invariant generation for (branching-free) loops with a single linear update. Our primary contribution is a polynomial-space algorithm that computes the strongest algebraic invariant for simple linear loops, generating all polynomial equations that hold among program variables across all reachable states. The key to achieving our complexity bounds lies in mitigating the blowup associated with variable elimination and Gr\"obner basis computation, as seen in prior works. Our procedure runs in polynomial time when the number of program variables is fixed. We examine various applications of our results on invariant generation, focusing on invariant verification and loop synthesis. The invariant verification problem investigates whether a polynomial ideal defining an algebraic set serves as an invariant for a given linear loop. We show that this problem is coNP-complete and lies in PSPACE when the input ideal is given in dense or sparse representations, respectively. In the context of loop synthesis, we aim to construct a loop with an infinite set of reachable states that upholds a specified algebraic property as an invariant. The strong synthesis variant of this problem requires the construction of loops for which the given property is the strongest invariant. In terms of hardness, synthesising loops over integers (or rationals) is as hard as Hilbert's Tenth problem (or its analogue over the rationals). When loop constants are constrained to bit-bounded rational numbers, we demonstrate that loop synthesis and its strong variant are both decidable in PSPACE, and in NP when the number of program variables is fixed.

翻译：自动生成循环不变量是软件验证中的一个基础性难题。尽管该任务在一般情况下是不可判定的，但对于某些受限的程序类别却是可判定的。本文主要研究具有单一线性更新的（无分支）循环的不变量生成。我们的核心贡献是提出了一种多项式空间算法，该算法能够计算简单线性循环的最强代数不变量，生成所有在可达状态间关于程序变量均成立的多项式方程。实现我们复杂度界限的关键在于缓解先前工作中出现的、与变量消元和Gröbner基计算相关的规模爆炸问题。当程序变量数量固定时，我们的过程在多项式时间内运行。我们探讨了不变量生成结果的多种应用，重点关注不变量验证和循环综合。不变量验证问题研究的是定义一个代数集的多项式理想是否可作为给定线性循环的不变量。我们证明，当输入理想分别以稠密或稀疏表示给定时，该问题是coNP完全的且属于PSPACE。在循环综合的背景下，我们的目标是构造一个具有无限可达状态集、且能将指定代数性质作为不变量保持的循环。该问题的强综合变体要求构造出使给定性质成为最强不变量的循环。在难度方面，在整数（或有理数）上综合循环的难度与希尔伯特第十问题（或其有理数域上的类似问题）相当。当循环常数被限制为比特有界有理数时，我们证明循环综合及其强变体在PSPACE中都是可判定的，并且在程序变量数量固定时属于NP。