A Calculus for Modular Loop Acceleration

Frohn, Florian

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Paper

A Calculus for Modular Loop Acceleration

MPS-Authors

/persons/resource/persons253052

Frohn, Florian
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

arXiv:2001.01516.pdf
(Preprint), 320KB

Supplementary Material (public)

There is no public supplementary material available

Citation

Frohn, F. (2020). A Calculus for Modular Loop Acceleration. Retrieved from https://arxiv.org/abs/2001.01516.

Cite as: https://hdl.handle.net/21.11116/0000-0007-CEFC-6

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.