Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the problem is in general undecidable, the goal is settled for restricted classes of loops. For the class of solvable loops, introduced by Kapur and Rodr\'iguez-Carbonell in 2004, one can automatically compute invariants from closed-form solutions of recurrence equations that model the loop behaviour. In this paper we establish a technique for invariant synthesis for loops that are not solvable, termed unsolvable loops. Our approach automatically partitions the program variables and identifies the so-called defective variables that characterise unsolvability. Herein we consider the following two applications. First, we present a novel technique that automatically synthesises polynomials from defective monomials, that admit closed-form solutions and thus lead to polynomial loop invariants. Second, given an unsolvable loop, we synthesise solvable loops with the following property: the invariant polynomials of the solvable loops are all invariants of the given unsolvable loop. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.

翻译：自动生成不变量是概率性与确定性程序计算机辅助分析及编译器优化的关键，但仍是一个具有挑战性的开放性问题。尽管该问题在一般情况下不可判定，但对于受限循环类已取得解决。对于2004年Kapur和Rodríguez-Carbonell提出的可解循环类，可通过建模循环行为的递推方程闭式解自动计算不变量。本文建立了一种针对不可解循环（即非可解循环）的不变量合成技术。我们的方法自动划分程序变量，并识别表征不可解性的所谓缺陷变量。本文考虑以下两个应用：首先，提出一种新技术，能从缺陷单项式中自动合成具有闭式解的多项式，从而生成多项式循环不变量；其次，给定不可解循环，我们合成满足以下性质的可解循环：可解循环的不变多项式均为给定不可解循环的全部不变量。我们的实现与实验证明了该方法在确定性与概率性程序中的可行性与适用性。