This is the empirical evaluation of the papers *A Calculus for Modular Loop Acceleration* and *A Calculus for Modular Loop Acceleration and Non-Termination Proofs*.
You can find the source code for our tool LoAT at GitHub.

Moreover, we refer to the general LoAT website for further information.

# A Calculus for Modular Loop Acceleration

## Artifact Evaluation

Here you can find the zip-file for the artifact evaluation committee.## Downloading LoAT

We provide a pre-compiled binary of LoAT (Linux, 64 bit). Apart from that, LoAT is open-source and the source code of the version that was used for our evaluation is available on Github.

## Examples

- 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.

## Evaluation

### StarExec-Jobs

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

- full version of our acceleration calculus
- Invocation:
`loat-static $INPUT`

- Invocation:
*acceleration via monotonicity*- Invocation:
`loat-static --acceleration mon $INPUT`

- Invocation:
*acceleration via metering functions*- Invocation:
`loat-static --acceleration meter $INPUT`

- Invocation:
- restricted version of our acceleration calculus without
*acceleration via eventual increase*- Invocation:
`loat-static --acceleration no-ev-inc $INPUT`

- Invocation:
- restricted version of our acceleration calculus without
*acceleration via eventual decrease*- Invocation:
`loat-static --acceleration no-ev-dec $INPUT`

- Invocation:
- 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`

- Invocation:
- Flata
- Invocation:
`java -cp flata.jar:antlr-3.3-complete.jar:nts.jar verimag.main.Calculator input.rel -noGLPK`

- Invocation:

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.

### LoAT's Output

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.

### Flata's Results

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.

### Zip-Files with Results

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

### Detailed Results

Below we provide tables with the detailed results of our benchmarks:- LoAT
*acceleration via monotonicity**acceleration via metering functions*- Flata
- LoAT without
*acceleration via eventual increase* - LoAT without
*acceleration via eventual decrease* - LoAT without
*acceleration via eventual increase*and*acceleration via eventual decrease*

### LoAT's Input Format

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

Here, the updates to the variables `x_1`

, ..., `x_d`

are *simultaneous*:
For example, if we have assignments `x_1 := x_1 + 1`

and `x_2 := x_1`

, the new value of `x_2`

will be the value that `x_1`

had *before* the assignment `x_1 := x_1 + 1`

in the current loop iteration.

# A Calculus for Modular Loop Acceleration and Non-Termination Proofs

For our evaluation of our novel calculus for loop acceleration, see above. In the following, we provide information about the evaluation of our novel calculus for proving non-termination.

## Downloading LoAT

We provide a pre-compiled binary of LoAT (Linux, 64 bit). Apart from that, LoAT is open-source and the source code of the version that was used for our evaluation is available on Github.

## Examples

- Here you can find the loops that we used for our evaluation.
- Here you can find the loops that we used for our evaluation as
`C`

programs. - Here you can find the examples from our paper.

The examples that could not be solved by any tool in our evaluation are:

`1567523084804575.koat`

`1567523106272845.koat`

`1567523084803520.koat`

`1567523039443195.koat`

## Evaluation

### Versions of Other Tools

- For AProVE, we used a custom version provided by its developers.
- For iRankFinder, we used the version from the termination competition 2021.
- For RevTerm, we used the version with SHA
`45e96f9`

from the GitHub repository. - For Ultimate, we used the version from the termination competition 2021.
- For VeryMax, we used the version from the termination competition 2019.

### Invoking the Tools

Below we show how to invoke the different tools and configurations that we evaluated.

- LoAT:
`loat-static --mode recurrent_set $INPUT`

- AProVE:
`java -Xmx14G -Xms14G -ea -jar aprove.jar -m wst -w 4 $INPUT`

- AProVE NT:
`java -Xmx14G -Xms14G -ea -jar aprove.jar -m wst -w 4 -s llvm-nonterm.strategy $INPUT`

- you can find the file
`llvm-nonterm.strategy`

here

- you can find the file
- iRankFinder: StarExec-configuration
`competition`

- iRankFinder NT:
`irankfinder -nt monotonicrecset -f $INPUT`

- RevTerm: we used the following two invocations, where the first one was wrapped with
`timeout 30`

`RevTerm.sh $INPUT -linear part1 mathsat 2 1`

`RevTerm.sh $INPUT -linear part2 mathsat 2 1`

- Ultimate: StarExec-Configuration
`default`

- VeryMax: StarExec-Configuration
`termcomp19_ITS`

- LoAT without
*monotonic increase*:`loat-static --mode recurrent_set_no_inc $INPUT`

- LoAT without
*eventual increase*:`loat-static --mode recurrent_set_no_ev_inc $INPUT`

- LoAT without
*fixpoints*:`loat-static --mode recurrent_set_no_fp $INPUT`

- LoAT without
*eventual increase*and*fixpoints*:`loat-static --mode recurrent_set_trivial $INPUT`