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.

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