论文标题
模块化循环加速的演算
A Calculus for Modular Loop Acceleration
论文作者
论文摘要
循环加速度可用于证明安全性，可及性，运行时界限和（不）在整数上运行的程序。为此，已经提出了多种加速技术。但是，它们都是整体的：他们要么成功地加速了循环，要么完全失败。相比之下，我们提出了一个微积分，该积分允许以模块化方式组合加速技术，并展示了如何将许多现有的加速技术集成到我们的微积分中。此外，我们提出了两种新型的加速技术，可以将它们无缝地纳入我们的微积分中。经验评估证明了我们方法的适用性。
Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs operating on integers. To this end, a variety of acceleration techniques has been proposed. However, all of them are monolithic: Either they accelerate a loop successfully or they fail completely. In contrast, we present a calculus that allows for combining acceleration techniques in a modular way and we show how to integrate many existing acceleration techniques into our calculus. Moreover, we propose two novel acceleration techniques that can be incorporated into our calculus seamlessly. An empirical evaluation demonstrates the applicability of our approach.
