一句话：提出一种可处理非尾递归的整数程序最坏情况运行时下界推断技术，并在工具 LoAT 中实现。
该文研究整数程序最坏情况运行时间的下界推断。与此前工作不同，方法不局限于尾递归。作者利用迭代的、欠近似程序化简框架构造程序执行的符号表示，其核心是基于递推求解和一种 ranking function 变体的欠近似程序加速；随后通过专用演算与 SMT 编码从化简后的程序推导渐近下界。作者在工具 LoAT 中实现该技术，并在大量例子中成功推断出非平凡的下界，表明其适用性超出尾递归情形。
We present a technique to infer lower bounds on the worst-case runtime complexity of integer programs, where in contrast to earlier work, our approach is not restricted to tail-recursion. Our technique constructs symbolic representations of program executions using a framework for iterative, under-approximating program simplification. The core of this simplification is a method for (under-approximating) program acceleration based on recurrence solving and a variation of ranking functions. Afterwards, we deduce asymptotic lower bounds from the resulting simplified programs using a special-purpose calculus and an SMT encoding. We implemented our technique in our tool LoAT and show that it infers non-trivial lower bounds for a large class of examples.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1911-01077,
title = {Inferring Lower Runtime Bounds for Integer Programs},
author = {Florian Frohn and Matthias Naaf and Marc Brockschmidt and Jürgen Giesl},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {42},
number = {3},
year = {2020},
doi = {10.1145/3410331}
}