论文标题
解决不可循环的不变生成
Solving Invariant Generation for Unsolvable Loops
论文作者
论文摘要
自动生成不变性，这是对概率和确定性程序的计算机辅助分析以及编译器优化的关键，这是一个具有挑战性的开放问题。尽管这个问题通常是不可决定的，但目标是针对限制的循环。对于Kapur和Rodríguez-Carbonell在2004年推出的可解决的循环类别，可以自动从对环行为进行模拟的复发方程的封闭形式溶液中自动计算不变性。在本文中，我们建立了一种用于不可解决的循环的不变合成技术，称为无法解析的循环。我们的方法会自动对程序变量进行划分，并标识表征无法解释性的所谓有缺陷变量。我们进一步提出了一种新型技术，该技术自动在有缺陷的变量中自动合成多项式，该变量允许封闭形式的溶液，从而导致多项式回路不变。我们的实施和实验既证明了我们对确定性和概率计划的方法的可行性和适用性。
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íguez-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. We further present a novel technique that automatically synthesises polynomials, in the defective variables, that admit closed-form solutions and thus lead to polynomial loop invariants. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.
