一句话：刻画线性数值循环何时可用有理数上的多项式和指数表示闭式形式，并给出可判定的安全性与终止性验证过程。
本文研究简单数值循环非线性行为的推理问题，基于线性动力系统分析的经典技术。线性动力系统的闭式行为通常可用代数数表示，但这种公式不利于自动化推理。本文刻画了线性循环在何种条件下可在更简单的理论中获得闭式形式，并给出计算算法；算法避免使用代数数，而将闭式形式表示为有理数上的多项式和指数。作者证明该闭式表达逻辑是可判定的，从而得到一类有理数数值循环的安全性和终止性验证判定过程。此外，该闭式计算过程可用于对任意数值程序（控制流不受限、非确定性赋值和递归过程）的行为进行过近似。
This paper investigates the problem of reasoning about non-linear behavior of simple numerical loops. Our approach builds on classical techniques for analyzing the behavior of linear dynamical systems. It is well-known that a closed-form representation of the behavior of a linear dynamical system can always be expressed using algebraic numbers, but this approach can create formulas that present an obstacle for automated-reasoning tools. This paper characterizes when linear loops have closed forms in simpler theories that are more amenable to automated reasoning. The algorithms for computing closed forms described in the paper avoid the use of algebraic numbers, and produce closed forms expressed using polynomials and exponentials over rational numbers. We show that the logic for expressing closed forms is decidable, yielding decision procedures for verifying safety and termination of a class of numerical loops over rational numbers. We also show that the procedure for computing closed forms for this class of numerical loops can be used to over-approximate the behavior of arbitrary numerical programs (with unrestricted control flow, non-deterministic assignments, and recursive procedures).
@article{paperbot625,
title = {Closed forms for numerical loops},
author = {Zachary Kincaid and Jason Breck and John Cyphert and Thomas Reps},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290368}
}