## 1 Introduction

## 2 Preliminaries

^{1}\(\vec {x} \mapsto \vec {a}\) maps integers to integers. \( Loop \) denotes the set of all such loops.

## 3 Existing acceleration techniques

^{2}

### 3.1 Acceleration via decrease or increase

^{3}Then \(\{\vec {x} \in \mathbb {Z}^d \mid \varphi (\vec {x})\}\) is a recurrent set [36] (see also Sect. 8.2) of \(\mathcal {T}_{loop}\). In other words, this acceleration technique applies if \(I_{\varphi }\) is monotonically increasing w.r.t. \(\vec {a}\).

### 3.2 Acceleration via decrease and increase

### 3.3 Acceleration via metering functions

## 4 A calculus for modular loop acceleration

## 5 Conditional acceleration techniques

## 6 Acceleration via eventual monotonicity

### 6.1 Acceleration via eventual decrease

### 6.2 Acceleration via eventual increase

## 7 Proving non-termination via loop acceleration

## 8 Related work

### 8.1 Related work on acceleration

### 8.2 Related work on proving non-termination

## 9 Implementation and experiments

### 9.1 Loop acceleration

^{4}(which is also used in the category Complexity of Integer Transition Systems of the Termination and Complexity Competition) to Flata’s input format. Note that our benchmark collection contains 16 loops with non-linear arithmetic where Flata is bound to fail, since it supports only linear arithmetic. We did not compare with FAST [3], which uses a similar approach as the more recent tool Flata. We used a wall clock timeout of 60 s per example and a memory limit of 128GB for each tool.

LoAT | Monot. | Meter | Flata | |
---|---|---|---|---|

Exact | 1444 | 845 |
\(0^5\) | 1231 |

Approx | 38 | 0 | 733 | 0 |

Fail | 29 | 666 | 778 | 280 |

Avg rt | 0.16 s | 0.11 s | 0.09 s | 0.47 s |

Median rt | 0.09 s | 0.09 s | 0.09 s | 0.40 s |

SD rt | 0.18 s | 0.09 s | 0.03 s | 0.50 s |

Exact | 1444 | 845 | 845 |

Approx | 0 | 493 | 0 |

Fail | 67 | 173 | 666 |

Avg rt | 0.15s | 0.14s | 0.09s |

Median rt | 0.08s | 0.08s | 0.07s |

SD rt | 0.17s | 0.17s | 0.06s |

LoAT: | |

Monot.: | Acceleration via Monotonicity, Theorem 3 |

Meter: | Acceleration via Metering Functions, Theorem 4 |

Flata: | |

: | |

: | |

: | |

Exact: | Examples that were accelerated exactly |

Approx: | Examples that were accelerated approximately |

Fail: | Examples that could not be accelerated |

Avg rt: | Average wall clock runtime |

Median rt: | Median wall clock runtime |

SD rt: | Standard deviation of wall clock runtime |

LoAT | AProVE | AProVE NT | iRankFinder | iRankFinder NT | RevTerm | Ultimate | VeryMax | |
---|---|---|---|---|---|---|---|---|

No | 206 | 200 | 200 | 205 | 205 | 133 | 205 | 175 |

Yes | 0 | 1301 | 0 | 1298 | 0 | 0 | 919 | 1299 |

Fail | 1305 | 10 | 1311 | 8 | 1306 | 1378 | 387 | 37 |

Avg rt | 0.03 s | 16.09 s | 25.69 s | 1.40 s | 1.03 s | 38.85 s | 23.30 s | 3.17 s |

Avg rt No | 0.03 s | 10.65 s | 9.67 s | 1.34 s | 0.96 s | 4.63 s | 7.99 s | 14.52 s |

Median rt | 0.02 s | 13.41 s | 15.74 s | 1.11 s | 0.91 s | 34.93 s | 11.57 s | 0.03 |

Median rt No | 0.02 s | 8.51 s | 6.91 s | 1.17 s | 0.90 s | 1.88 s | 8.01 s | 5.36 s |

SD rt | 0.03 s | 10.09 s | 19.95 s | 2.25 s | 0.30 s | 16.61 s | 21.60 s | 10.76 s |

SD rt No | 0.06 s | 5.80 s | 5.80 s | 0.92 s | 0.12 s | 11.08 s | 1.88 s | 13.24 s |

^{5}

### 9.2 Non-termination

^{6}For iRankFinder and VeryMax, we transformed them into the format from the category Termination of Integer Transition Systems of the Termination and Complexity Competition [12]. The latter format is also supported by LoAT, so besides iRankFinder and VeryMax, we also used it to evaluate LoAT.

`RevTerm.sh prog.c-linear part1 mathsat 2 1 `

`RevTerm.sh prog.c-linear part2 mathsat 2 1 `

It is important to note that all tools but RevTerm and LoAT also try to prove termination. Thus, a comparison between the runtimes of LoAT and those other tools is of limited significance. Therefore, we also compared LoAT with configurations of the tools that only try to prove non-termination. For AProVE, such a configuration was kindly provided by its developers (named AProVE NT in Table 3). In the case of iRankFinder, the excellent documentation allowed us to easily build such a configuration ourselves (named iRankFinder NT in Table 3). In the case of Ultimate, its developers pointed out that a comparison w.r.t. runtime is meaningless, as it is dominated by Ultimate’s startup-time of
\({\sim } 10\) s on small examples. For VeryMax, it is not possible to disable termination-proving, according to its authors.^{7}

LoAT | |||||
---|---|---|---|---|---|

No | 206 | 206 | 203 | 205 | 0 |

Fail | 1305 | 1305 | 1308 | 1306 | 1511 |

Avg rt | 0.03 s | 0.03 s | 0.03 s | 0.03 s | 0.02 s |

Avg rt No | 0.03 s | 0.02 s | 0.02 s | 0.02 s | – |

Median rt | 0.02 s | 0.02 s | 0.02 s | 0.02 s | 0.02 s |

Median rt No | 0.02 s | 0.02 s | 0.02 s | 0.02 s | – |

SD rt | 0.03 s | 0.02 s | 0.02 s | 0.02 s | 0.02 s |

SD rt No | 0.06 s | 0.03 s | 0.03 s | 0.04 s | – |

LoAT: | Calculus from Section 7 |

AProVE: | |

AProVE NT: | Configuration of AProVE that does not try to prove termination |

iRankFinder: | |

iRankFinder NT: | Configuration of iRankFinder that does not try to prove termination |

RevTerm: | |

Ultimate: | |

VeryMax: | |

: | |

: | |

: | |

: | |

NO: | Number of non-termination proofs |

YES: | Number of termination proofs |

Fail: | Number of examples where (non-)termination could not be proven |

Avg rt: | Average wall clock runtime |

Avg rt NO: | Average wall clock runtime when non-termination was proven |

Median rt: | Median wall clock runtime |

Median rt NO: | Median wall clock runtime when non-termination was proven |

SD rt: | Standard deviation of wall clock runtime |

SD rt NO: | Standard deviation of wall clock runtime when non-termination was proven |