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. Some of these acceleration techniques apply only to non-terminating loops. Thus, combining them with our novel calculus results in a new, modular approach for proving non-termination. An empirical evaluation demonstrates the applicability of our approach, both for loop acceleration and for proving non-termination.
翻译:循环加速可以用来证明以整数操作的程序的安全性、可达性、运行时间界限和(非)终止。 为此,已经提出了各种加速技术。 但是,所有这些技术都是单一的:它们要么成功地加速环绕,要么完全失败。相反,我们提出了一个微积分,允许以模块方式将加速技术结合起来,我们展示了如何将许多现有的加速技术纳入我们的微积分。此外,我们提出了两种新的加速技术,可以无缝地融入我们的微积分中。其中一些加速技术只适用于非终止环。因此,将它们与我们的新微积分相结合,形成一种新的模块化方法来证明非终止。一项实证性评价显示了我们的方法,即循环加速和证明非终止的实用性。