We provide a pre-compiled binary of LoAT (Linux, 64 bit). Apart from that, LoAT is open-source and available on Github

- Here you can find the loops that we used for our evaluation.
- Here you can find the loops that we used for our evaluation in Flata's input format.
- Here you can find the examples from our paper.

Below we provide links to the StarExec-Jobs of our evaluation.

- full version of our acceleration calculus
- Invocation:
`loat-static $INPUT` *acceleration via monotonicity*- Invocation:
`loat-static --acceleration mon $INPUT` *acceleration via metering functions*- Invocation:
`loat-static --acceleration meter $INPUT` - restricted version of our acceleration calculus without
*acceleration via eventual increase* - Invocation:
`loat-static --acceleration no-ev-inc $INPUT` - restricted version of our acceleration calculus without
*acceleration via eventual decrease* - Invocation:
`loat-static --acceleration no-ev-dec $INPUT` - restricted version of our acceleration calculus without
*acceleration via eventual increase*and without*acceleration via eventual decrease* - Invocation:
`loat-static --acceleration no-ev-mon $INPUT` - Flata
- Invocation:
`java -cp flata.jar:antlr-3.3-complete.jar:nts.jar verimag.main.Calculator input.rel -noGLPK`

In the tables on StarExec, the result "YES" means that the loop in question was accelerated exactly, "MAYBE" means that it was accelerated approximately, and "NO" means that the tool failed to accelerate it. By clicking on one of the examples and unfolding "output", you can see the full output of the tool.

If the loop was accelerated successfully, then the end of the output looks, e.g., as follows:

`
0.00/0.12 Start location: start
0.00/0.12 0: start -> f : [], cost: 0
0.00/0.12 2: f -> f : x'=-n+x, x_1'=n+x_1, x_2'=x_3, x_4'=x_5, [ n>0 && 1+x_1>0 && x_3>0 && x_2>0 && 1-n+x>0 && -1+x_4>0 && -1+x_5>0 ], cost: 1
0.00/0.12 EOF
`

The leading `0.00/0.12` is a timestamp which is added by StarExec and can thus be ignored, just as the trailing `EOF`.
The accelerated loop is presented in a rule-based formalism, which is equivalent to the formulas that are used in the paper.
It is always prefixed by `c: f -> f` where `c` is a natural number.
The remainder of the corresponding line above is equivalent to the formula

`x'=-n+x && x_1'=n+x_1 && x_2'=x_3 && x_4'=x_5 && n>0 && 1+x_1>0 && x_3>0 && x_2>0 && 1-n+x>0 && -1+x_4>0 && -1+x_5>0`.

The costs are irrelevant for our paper and can thus be ignored.

The invocation of Flata was suggested by its developers. Note that Flata sometimes failed with one of the following two errors:

`Exception in thread "main" verimag.flata.common.NotPresburger``no viable alternative at character '2'`

This happens when the loop contains non-linear arithmetic, which is not supported by Flata.

As StarExec might be temporarily unavailable due to updates, we also provide zip-files with the results and the full output of LoAT and Flata.

- full version of our acceleration calculus
*acceleration via monotonicity**acceleration via metering functions*- restricted version of our acceleration calculus without
*acceleration via eventual increase* - restricted version of our acceleration calculus without
*acceleration via eventual decrease* - restricted version of our acceleration calculus without
*acceleration via eventual increase*and without*acceleration via eventual decrease* - Flata

LoAT uses the input format of the tool KoAT (file ending .koat). It represents programs as transition systems, using a rule-based formalism. An example for a valid input is:

`
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS start))
(VAR x y z)
(RULES
start(x, y, z) -> f(x, y, z)
f(x, y, z) -> f(x-1, y+x, z-y) [x > 0 && y > 0 && z > 0]
)
`

The first line is needed for historical reasons and is meaningless in the context of our paper.

The second line declares the entry-point of the program. Note that KoAT's input format requires that each program has a unique entry-point without any incoming transitions (i.e., in the example above, a rule where `start` occurs on the
right-hand side would be invalid).

In the third line, the program variables are declared.

For the purpose of our paper, the `RULES`-section always contains two rules: One of the form

`
start(...) -> f(...),
`

which is needed due to the requirement that the entry-point of the program does not have incoming transitions (see above), and a second rule

`
f(x_1,...,x_d) -> f(t_1,...,t_d) [phi],
`

which represents the loop that should be accelerated. More precisely, it represents the following loop:

`
while (phi)
x_1 := t_1
...
x_d := t_d
`