@online{Frohn_arXiv2001.01516,
TITLE = {A Calculus for Modular Loop Acceleration},
AUTHOR = {Frohn, Florian},
LANGUAGE = {eng},
URL = {https://arxiv.org/abs/2001.01516},
EPRINT = {2001.01516},
EPRINTTYPE = {arXiv},
YEAR = {2020},
ABSTRACT = {Loop acceleration can be used to prove safety, reachability, runtime bounds,<br>and (non-)termination of programs operating on integers. To this end, a variety<br>of acceleration techniques has been proposed. However, all of them are<br>monolithic: Either they accelerate a loop successfully or they fail completely.<br>In contrast, we present a calculus that allows for combining acceleration<br>techniques in a modular way and we show how to integrate many existing<br>acceleration techniques into our calculus. Moreover, we propose two novel<br>acceleration techniques that can be incorporated into our calculus seamlessly.<br>An empirical evaluation demonstrates the applicability of our approach.<br>},
}