A calculus for modular loop acceleration and non-termination proofs

International Journal on Software Tools for Technology Transfer, vol. 24, pp. 691–715

Abstract

Abstract Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs. To this end, a variety of acceleration techniques have been proposed. However, so far all of them have been monolithic, i.e., a single loop could not be accelerated using a combination of several different acceleration techniques. 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.

Authors 2

1. Florian Frohn corresponding Aachen LuFG Informatik 2

   RWTH Aachen University · Max Planck Institute for Informatics

   Affiliation as printed

   LuFG Informatik 2, RWTH Aachen University, Aachen, Germany

   Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbrücken, Germany

2. Carsten Fuhs

   Birkbeck, University of London

   Affiliation as printed

   Department of Computer Science and Information Systems, Birkbeck, University of London, London, UK