论文标题
证明非终止和较低的运行时间范围（系统描述）
Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)
论文作者
论文摘要
我们介绍了LOOP加速工具（LOAT）的新版本，该工具是在整数上运行的程序，用于证明非终止和最差的下限。它基于一种新颖的循环加速度演算，即将循环转换为非确定性的直线代码，并用于查找非末端配置。为了有效地实施它，Loat使用基于SMT解决和Unsat内核的新方法。一项广泛的评估表明，Loat与其他最先进的工具具有很高的竞争性，以证明未终止。尽管没有其他工具能够针对完整的整数程序推断出最差的下限，但我们也证明了Loat的表现可以大大优于其前任。
We present the new version of the Loop Acceleration Tool (LoAT), a powerful tool for proving non-termination and worst-case lower bounds for programs operating on integers. It is based on a novel calculus for loop acceleration, i.e., transforming loops into non-deterministic straight-line code, and for finding non-terminating configurations. To implement it efficiently, LoAT uses a new approach based on SMT solving and unsat cores. An extensive evaluation shows that LoAT is highly competitive with other state-of-the-art tools for proving non-termination. While no other tool is able to deduce worst-case lower bounds for full integer programs, we also demonstrate that LoAT significantly outperforms its predecessors.
