hide
Free keywords:
Computer Science, Logic in Computer Science, cs.LO,Computer Science, Programming Languages, cs.PL
Abstract:
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.
