A Calculus for Modular Loop Acceleration
Florian Frohn
Max Planck Institute for Informatics
Saarland Informatics Campus, Saarbr¨ ucken, Germany
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.
1 Introduction
In the last years, loop acceleration techniques have successfully been used to build
static analyses for programs operating on integers [2, 8, 11, 16–18, 28]. Essentially,
such techniques extract a quantifier-free first-order formula ψ from a single-path
loop T , i.e., a loop without branching in its body, such that ψ under-approximates
(resp. is equivalent to) T . More specifically, each model of the resulting formula ψ
corresponds to an execution of T (and vice versa). By integrating such techniques
into a suitable program-analysis framework [3, 11, 16–18, 23], whole programs
can be transformed into first-order formulas which can then be analyzed by
off-the-shelf solvers. Applications include proving safety [23] or reachability
[23, 28], deducing bounds on the runtime complexity [16, 17], and proving (non-)
termination [8, 11].
However, existing acceleration techniques only apply if certain prerequisites
are in place. So the power of static analyses built upon loop acceleration depends
on the applicability of the underlying acceleration technique.
In this paper, we introduce a calculus which allows for combining several acceleration techniques modularly in order to accelerate a single loop. Consequently,
it can handle classes of loops where all standalone techniques fail. Moreover, we
present two novel acceleration techniques and integrate them into our calculus.
In the following, we introduce preliminaries in Sec. 2. Then, we discuss existing
acceleration techniques in Sec. 3. In Sec. 4, we present our calculus to combine
acceleration techniques. Sec. 5 shows how existing acceleration techniques can be
This work has been funded by DFG grant 389792660 as part of TRR 248 (see
https://perspicuous-computing.science).
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 58–76, 2020.
https://doi.org/10.1007/978-3-030-45190-5 4
TACAS
Evaluation
Artifact
2020
Accepted
Florian Frohn
Max Planck Institute for Informatics
Saarland Informatics Campus, Saarbr¨ ucken, Germany
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.
1 Introduction
In the last years, loop acceleration techniques have successfully been used to build
static analyses for programs operating on integers [2, 8, 11, 16–18, 28]. Essentially,
such techniques extract a quantifier-free first-order formula ψ from a single-path
loop T , i.e., a loop without branching in its body, such that ψ under-approximates
(resp. is equivalent to) T . More specifically, each model of the resulting formula ψ
corresponds to an execution of T (and vice versa). By integrating such techniques
into a suitable program-analysis framework [3, 11, 16–18, 23], whole programs
can be transformed into first-order formulas which can then be analyzed by
off-the-shelf solvers. Applications include proving safety [23] or reachability
[23, 28], deducing bounds on the runtime complexity [16, 17], and proving (non-)
termination [8, 11].
However, existing acceleration techniques only apply if certain prerequisites
are in place. So the power of static analyses built upon loop acceleration depends
on the applicability of the underlying acceleration technique.
In this paper, we introduce a calculus which allows for combining several acceleration techniques modularly in order to accelerate a single loop. Consequently,
it can handle classes of loops where all standalone techniques fail. Moreover, we
present two novel acceleration techniques and integrate them into our calculus.
In the following, we introduce preliminaries in Sec. 2. Then, we discuss existing
acceleration techniques in Sec. 3. In Sec. 4, we present our calculus to combine
acceleration techniques. Sec. 5 shows how existing acceleration techniques can be
This work has been funded by DFG grant 389792660 as part of TRR 248 (see
https://perspicuous-computing.science).
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 58–76, 2020.
https://doi.org/10.1007/978-3-030-45190-5 4
TACAS
Evaluation
Artifact
2020
Accepted