We present the Polar framework for fully automating the analysis of classical and probabilistic loops using algebraic reasoning. The central theme in Polar comes with handling algebraic recurrences that precisely capture the loop semantics. To this end, our work implements a variety of techniques to compute exact closed-forms of recurrences over higher-order moments of variables, infer invariants, and derive loop sensitivities with respect to unknown parameters. Polar can analyze probabilistic loops containing if-statements, polynomial arithmetic, and common probability distributions. By translating loop analysis into linear recurrence solving, Polar uses the derived closed-forms of recurrences to compute the strongest polynomial invariant or to infer parameter sensitivity. Polar is both sound and complete within well-defined programming model restrictions. Lifting any of these restrictions results in significant hardness limits of computation. To overcome computational burdens for the sake of efficiency, Polar also provides incomplete but sound techniques to compute moments of combinations of variables.

翻译：本文提出Polar框架，通过代数推理实现经典循环与概率循环分析的完全自动化。Polar的核心思想在于处理能够精确刻画循环语义的代数递推式。为此，我们实现了多种技术以计算变量高阶矩的精确闭式解、推断不变量，并推导循环对未知参数的敏感度。Polar能够分析包含条件语句、多项式运算及常见概率分布的概率循环。通过将循环分析转化为线性递推式求解，Polar利用推导出的递推闭式解计算最强多项式不变量或推断参数敏感度。在明确定义的程序模型限制下，Polar具备可靠性与完备性。任何限制条件的放宽都将导致计算复杂度的显著提升。为提升计算效率以克服计算负担，Polar同时提供了不完整但可靠的技术来计算变量组合的矩。