Proving Non-Termination via Loop Acceleration

TL;DR

This paper introduces a novel approach to proving non-termination of integer programs using loop acceleration, which also helps find paths to other non-terminating loops, enhancing automated analysis.

Contribution

It presents the first non-termination proof method based on loop acceleration, including a new invariant inference technique and a unified transformation framework.

Findings

The approach is fully automated and competitive with existing methods.

The technique successfully proves non-termination in various benchmark programs.

It can also accelerate loops to discover non-termination paths.

Abstract

We present the first approach to prove non-termination of integer programs that is based on loop acceleration. If our technique cannot show non-termination of a loop, it tries to accelerate it instead in order to find paths to other non-terminating loops automatically. The prerequisites for our novel loop acceleration technique generalize a simple yet effective non-termination criterion. Thus, we can use the same program transformations to facilitate both non-termination proving and loop acceleration. In particular, we present a novel invariant inference technique that is tailored to our approach. An extensive evaluation of our fully automated tool LoAT shows that it is competitive with the state of the art.

Equations

$$\begin{array}[]{l@{\qquad\quad}rlll}\alpha_{1}:&\mathsf{start}(x,y)&\to&\mathsf{f}(x,y)\\ \alpha_{2}:&\mathsf{f}(x,y)&\to&\mathsf{f}(x-y,y+1)&\ \left[x\geq 0\right]\\ \alpha_{3}:&\mathsf{f}(x,y)&\to&\mathsf{g}(x,y)&\ \left[x<0\right]\\ \alpha_{4}:&\mathsf{g}(x,y)&\to&\mathsf{g}(x,y-x)&\ \left[y>0\right]\end{array}$$

$$\begin{array}[]{lll}\text{if }&\mathsf{start}(\bm{n})\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$

}}}{\scriptstyle\,}}}^{*}_{\operatorname{proc}(\mathcal{T})}\omega&\text{or }\\ &\lx@intercol\mathsf{start}(\bm{n})\text{ witnesses non-termination of }\operatorname{proc}(\mathcal{T}),\hfil\lx@intercol\\ \text{then }&\mathsf{start}(\bm{n})\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{

$$}}}{\scriptstyle\,}}}^{*}_{\mathcal{T}}\omega&\text{or }\\ &\lx@intercol\mathsf{start}(\bm{n})\text{ witnesses non-termination of }\mathcal{T}.\hfil\lx@intercol\end{array}$$

$$\forall \mathcal{V}(\mathcal{T}).{\mathrm{guard}}_{\alpha }\wedge {\phi }_{ci}⟹{\mathrm{up}}_{\alpha }({\phi }_{ci})$$

$$\forall \mathcal{V}(\mathcal{T}).{\phi }_{si}⟹{\mathrm{up}}_{\alpha }({\phi }_{si})$$

$$\forall \mathcal{V}(\mathcal{T}).{\phi }_{si}\wedge {\mathrm{up}}_{\alpha }({\phi }_{md})⟹{\phi }_{md}$$

$$\begin{array}[]{llll}\forall x,y.\ y\geq 0&\implies&y+1\geq 0&\text{and}\\ \forall x,y.\ y\geq 0\mathrel{\land}x-y\geq 0&\implies&x\geq 0\end{array}$$

$$\overline{\alpha}=\boxed{\mathsf{f}(\bm{x})\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$

}}}{\scriptstyle\,}}}\mathsf{f}(\mu(\bm{x}))\ \left[\varphi_{ci}\mathrel{\land}\varphi_{si}\mathrel{\land}\operatorname{dec}_{\mathit{k}}(\mu(\varphi_{md}))\mathrel{\land}\mathit{k}\!>\!0\right]}\;.$$

$${\mathrm{up}}_{\alpha }^n({\phi }_{si})\text{ for all }n\in \mathbb{N}.$$

$${\mathrm{up}}_{\alpha }^n({\phi }_{md})\text{ for all }0\le n<k.$$

$${\mathrm{up}}_{\alpha }^n({\phi }_{ci})\text{ for all }0\le n\le k.$$

$$\overline{\alpha}_{2}:\quad\mathsf{f}(x,y)\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$

}}}{\scriptstyle\,}}}\mathsf{f}(\underbrace{x-y\cdot\mathit{k}-\tfrac{1}{2}\cdot\mathit{k}^{2}+\tfrac{1}{2}\cdot\mathit{k}}_{\mu(x)},\;\underbrace{y+\mathit{k}\vphantom{\tfrac{1}{2}}}_{\mu(y)})\ \left[\eta\right]$$

$$\alpha\circ\beta=\boxed{\operatorname{lhs}_{\alpha}\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$

}}}{\scriptstyle\,}}}\operatorname{up}_{\alpha}(\operatorname{rhs}_{\beta})\ \left[\operatorname{guard}_{\alpha}\mathrel{\land}\operatorname{up}_{\alpha}(\operatorname{guard}_{\beta})\right]}\;.$$

$${\alpha }_{neg}:\mathsf{f}(x,y)\to \mathsf{f}(-x,y-1)\left[y>x\right]$$

$$\alpha_{neg}\circ\alpha_{neg}:\quad\mathsf{f}(x,y)\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$

}}}{\scriptstyle\,}}}\mathsf{f}(x,y-2)\ \left[y>x\mathrel{\land}y-1>-x\right].$$

$$\mathsf{f}(x,y)\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$

}}}{\scriptstyle\,}}}\mathsf{f}(x,y-2\cdot\mathit{k})\ \left[\operatorname{dec}_{\mathit{k}}(\mu(\operatorname{guard}_{\alpha_{neg}\circ\alpha_{neg}}))\mathrel{\land}\mathit{k}>0\right]$$

$$y-2\cdot (k-1)>x\wedge y-2\cdot (k-1)-1>-x,$$

$${\alpha }_{const}:\mathsf{f}(x,y,z)\to \mathsf{f}(x-1,2,y)\left[x>0\right]$$

$${\alpha }_{const}\circ {\alpha }_{const}:\mathsf{f}(x,y,z)\to \mathsf{f}(x-2,2,2)\left[x>1\right]$$

$$\mathsf{f}(x,y,z)\to \mathsf{f}(x-2\cdot k,2,2)\left[x-2\cdot (k-1)>1\wedge k>0\right],$$

$${\alpha }_p:\mathsf{f}(x,y)\to \mathsf{f}(y-1,x-1)\left[x>0\right]$$

$${\alpha }_p\circ {\alpha }_p:\mathsf{f}(x,y)\to \mathsf{f}(x-2,y-2)\left[x>0\wedge y-1>0\right]$$

$$\mathsf{f}(x,y)\to \mathsf{f}(x-2\cdot k,y-2\cdot k)\left[{\mathrm{dec}}_k(\mu ({\mathrm{guard}}_{{\alpha }_p\circ {\alpha }_p}))\wedge k>0\right]$$

$$\{x\in \mathcal{V}({\mathrm{lhs}}_{\alpha })\mid \mathcal{V}({\mathrm{up}}_{\alpha }(x))\ne \varnothing \wedge x\notin \mathcal{V}({\mathrm{up}}_{\alpha }(x))\}.$$

$$\alpha^{\omega}=\boxed{\textstyle\operatorname{lhs}_{\alpha}\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$

}}}{\scriptstyle\,}}}\omega\ \left[\operatorname{guard}_{\alpha}\right]}\;.$$

$$\alpha_{4}^{\omega}:\quad\mathsf{g}(x,y)\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$

}}}{\scriptstyle\,}}}\omega\ \left[y>0\mathrel{\land}x\leq 0\right].$$

$${\alpha }_{nt}:\mathsf{f}(x,y)\to \mathsf{f}(0,y-x)\left[y>0\right]$$

$${\alpha }_{nt}\circ {\alpha }_{nt}:\mathsf{f}(x,y)\to \mathsf{f}(0,y-x)\left[y>0\wedge y-x>0\right].$$

$$\mathsf{f}(x,y)\to \omega \left[y>0\wedge y-x>0\right].$$

$${\alpha }^{\mathbf{f}\mathbf{p}}=\boxed{{\mathrm{lhs}}_{\alpha }\to \omega \left[{\mathrm{guard}}_{\alpha }\wedge \mathbf{x}={\mathrm{up}}_{\alpha }(\mathbf{x})\right]}.$$

$${\alpha }_1\circ {\overline{\alpha }}_2:\mathsf{start}(x,y)\to \mathsf{f}(x-y\cdot k-\frac{1}{2}\cdot k^2+\frac{1}{2}\cdot k,y+k)\text{hfill}\left[\eta \right]$$

Full text

I Introduction

Proving non-termination of integer programs is an important research topic (e.g., [14, 33, 13, 34, 2, 32, 26, 40, 7, 39]). In another line of research, under-approximating loop acceleration is used to analyze safety [30] and runtime complexity [21]. Here, the idea is to replace a loop by code that mimics $k$ loop iterations, where $k$ is chosen non-deterministically.

Many non-termination techniques first search for a diverging configuration and then prove its reachability. For the latter, loop acceleration would be useful, as it allows reasoning about paths with loops without fixing the number of unrollings. Still, up to now acceleration has not been used for non-termination proving.

To fill this gap, we design a novel loop acceleration technique whose prerequisites generalize a well-known non-termination criterion. This correspondence is of great value: It allows us to develop an under-approximating program simplification framework that progresses incrementally towards the detection of non-terminating loops and the acceleration of other loops.

After introducing preliminaries in Sect. II, we present our approach in Sect. III and IV. It eliminates loops via acceleration and chaining, or by proving their non-termination and replacing them by a transition to a special symbol $\omega$. If a loop cannot be eliminated, then we strengthen its guard by synthesizing suitable invariants. Our approach also handles nested loops by eliminating inner loops before removing outer loops. Eventually, this leads to a loop-free program where a trace to $\omega$ yields a witness of non-termination. So our main contributions are:

1. (a)

The applicability of existing under-approximating loop acceleration techniques is restricted: The technique from [30] is often inapplicable if the loop condition contains invariants and the technique from [21] requires metering functions which are often challenging to synthesize. Thus, in Sect. III we present a novel loop acceleration technique that generalizes [30] and does not require metering functions, and we integrate it into a program simplification framework inspired by [21]. 2. (b)

We combine our approach with a novel invariant inference technique in Sect. IV. So if the prerequisites of our nontermination criterion and our acceleration technique are violated, then we try to deduce invariants to make them applicable.

From a practical point of view, we contribute

1. (c)

an implementation in our open-source tool LoAT and 2. (d)

an extensive evaluation of our implementation, cf. Sect. V.

Finally, Sect. VI discusses related work and concludes. All proofs can be found in the appendix.

II Preliminaries

We denote vectors $\bm{x}$ by bold letters and the $i^{th}$ element of $\bm{x}$ by $x_{i}$. Transitions $\alpha$ have the form \mathsf{f}(\bm{x})\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$}}}{\scriptstyle\,}}}\mathsf{g}(\bm{t})\ \left[\eta\right]. The left-hand side $\operatorname{lhs}_{\alpha}=\mathsf{f}(\bm{x})$ consists of $\alpha$’s source function symbol $\operatorname{src}_{\alpha}=\mathsf{f}\in\Sigma$ and a vector of pairwise different variables $\bm{x}\subset\mathcal{V}$ ranging over $\mathbb{Z}$, where $\mathcal{V}$ is countably infinite. The set of function symbols $\Sigma$ is finite and we assume that all function symbols have the same arity (otherwise one can add unused arguments). We use $\mathcal{V}(\cdot)$ to denote all variables occurring in the argument. $\mathcal{A}$ denotes the set of all arithmetic expressions over $\mathcal{V}$, i.e., expressions built from variables, numbers, and arithmetic operations like “${+}$”, “${\cdot}$”, etc. The guard $\operatorname{guard}_{\alpha}=\eta$ is a constraint, i.e., a finite conjunction111Note that negations can be expressed by negating inequations directly, and disjunctions in programs can be expressed using several transitions. of inequations over $\mathcal{A}$, which we omit if it is empty. The right-hand side $\operatorname{rhs}_{\alpha}=\mathsf{g}(\bm{t})$ consists of $\alpha$’s destination $\operatorname{dest}_{\alpha}=\mathsf{g}\in\Sigma$ and a vector $\bm{t}\subset\mathcal{A}$. The substitution $\operatorname{up}_{\alpha}=\{\bm{x}\mapsto\bm{t}\}$ is $\alpha$’s update.

A substitution is a function $\sigma:\mathcal{V}\to\mathcal{A}$. The domain of $\sigma$ is $\operatorname{dom}(\sigma)=\{x\in\mathcal{V}\mid\sigma(x)\neq x\}$ and its range is defined as $\operatorname{rng}(\sigma)=\{\sigma(x)\mid x\in\operatorname{dom}(\sigma)\}$. We sometimes denote substitutions by sets of key-value pairs $\{y_{1}\mapsto t_{1},\ldots,y_{k}\mapsto t_{k}\}$ or just $\{\bm{y}\mapsto\bm{t}\}$. Then each $x\in\mathcal{V}\setminus\bm{y}$ is mapped to itself. For every entity $e$, $\sigma(e)$ results from replacing all free variables in $e$ according to $\sigma$. If $\operatorname{rng}(\sigma)\subset\mathbb{Z}$, then $\sigma$ is a valuation. A first-order formula $\varphi$ is valid if it is equivalent to $\mathsf{true}$. Moreover, a valuation $\sigma$ is a model of $\varphi$ (or satisfies $\varphi$, denoted $\sigma\models\varphi$) if $\sigma$’s domain contains all free variables of $\varphi$ and $\sigma(\varphi)$ is valid.

An integer program $\mathcal{T}$ is a finite set of transitions. Their guards restrict the control flow, i.e., \mathsf{f}(\bm{x})\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$}}}{\scriptstyle\,}}}\mathsf{g}(\bm{t})\ \left[\eta\right] is only applicable if the current valuation of the variables satisfies $\eta$.

Example 1** (Integer Program).**

Consider the function start:**

⬇

**def** start(x, y):

    **while** x >= 0: x = x - y; y = y + 1

    **while**  y > 0: y = y - x

It corresponds to the following integer program:

[TABLE]

The function symbols $\mathsf{f}$ and $\mathsf{g}$ represent the first and the second loop, respectively. The program does not terminate if, e.g., x and y are initially 0:* After applying the first loop twice, y is $2$ and x is $-1$, so that the second loop diverges.*

Definition 2** (Integer Transition Relation).**

A term $\mathsf{f}(\bm{n})$ where $\bm{n}\subset\mathbb{Z}$ is a configuration. An integer program $\mathcal{T}$ induces a relation ${\to_{\mathcal{T}}}$ on configurations: We have s\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$}}}{\scriptstyle\,}}}_{\mathcal{T}}t if there is an $\alpha\in\mathcal{T}$ and a model $\sigma$ of $\operatorname{guard}_{\alpha}$ such that $\mathcal{V}(\alpha)\subseteq\operatorname{dom}(\sigma)$, $\sigma(\operatorname{lhs}_{\alpha})=s$, and $\sigma(\operatorname{rhs}_{\alpha})=t$.222Throughout the paper, we use “${=}$” for semantic (not syntactic) equality w.r.t. arithmetic, e.g., “$\mathsf{f}(1+2)=\mathsf{f}(3)$” holds. Then we say that $s$ evaluates to $t$. As usual, {\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$}}}{\scriptstyle\,}}}^{*}_{\mathcal{T}}} is the transitive-reflexive closure of {\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$}}}{\scriptstyle\,}}}_{\mathcal{T}}}.

If there is an infinite {\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$}}}{\scriptstyle\,}}}_{\mathcal{T}}}-evaluation that starts with $\mathsf{start}(\bm{n})$ where $\mathsf{start}\in\Sigma$ is the canonical start symbol, then $\mathcal{T}$ is non-terminating and $\mathsf{start}(\bm{n})$ witnesses non-termination of $\mathcal{T}$.

W.l.o.g., $\mathsf{start}$ does not occur on right-hand sides. Otherwise, one can rename $\mathsf{start}$ to $\mathsf{start}^{\prime}$ and add a transition \mathsf{start}(\bm{x})\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$}}}{\scriptstyle\,}}}\mathsf{start}^{\prime}(\bm{x}). A program $\mathcal{T}$ is simplified if $\operatorname{src}_{\alpha}=\mathsf{start}$ for all $\alpha\in\mathcal{T}$. So any run of a simplified program has at most length one.

By definition, integer programs may contain transitions like \mathsf{f}(x)\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$}}}{\scriptstyle\,}}}\mathsf{f}(\frac{x}{2}). While evaluations that would not yield integers get stuck (as, e.g., $\mathsf{f}(\frac{1}{2})$ is not a configuration), our technique assumes that the arguments of functions are always integers. Hence, we restrict ourselves to well-formed integer programs.

Definition 3** (Well-Formedness).**

An integer program $\mathcal{T}$ is well formed if for all transitions $\alpha\in\mathcal{T}$ and all models $\sigma$ of $\operatorname{guard}_{\alpha}$ with $\mathcal{V}(\alpha)\subseteq\operatorname{dom}(\sigma)$, $\sigma(\operatorname{rhs}_{\alpha})$ is a configuration.

To ensure that the program is initially well formed, we just allow integers, addition, subtraction, and multiplication in the original program.333One could also allow expressions like $\frac{1}{2}\cdot x^{2}+\frac{1}{2}\cdot x$ in the initial program, as long as every arithmetic expression maps integers to integers. While our approach uses program transformations that may introduce further operations like division and exponentials, these transformations preserve well-formedness. We formalize our contributions in terms of processors.

Definition 4** (Processor).**

Let $\omega\in\Sigma$ be a dedicated fresh function symbol. A processor $\operatorname{proc}$ is a partial function which maps integer programs to integer programs. It is sound if the following holds for all $\mathcal{T}$ where $\operatorname{proc}$ is defined:

[TABLE]

If $\operatorname{proc}$ preserves well-formedness, then $\operatorname{proc}$ is called safe.

So we use the symbol $\omega$ to represent non-termination (and we omit its arguments for readability): If we can transform a program $\mathcal{T}$ into a simplified program $\mathcal{T}^{\prime}$ via safe and sound processors and $\sigma\models\operatorname{guard}_{\alpha}$ for some $\alpha\in\mathcal{T}^{\prime}$ with $\operatorname{rhs}_{\alpha}=\omega$, then $\sigma(\operatorname{lhs}_{\alpha})$ witnesses non-termination of $\mathcal{T}$ due to Def. 4.

III Simplifying Integer Programs

We now present our Contribution (a) by defining suitable processors. In Sect. III-A, we introduce the notions of invariants which are the foundation of our loop acceleration technique, cf. Sect. III-B. The remaining processors of our approach are used to combine transitions (Sect. III-C) and to finally deduce non-termination (Sect. III-D).

III-A Invariants

Our novel loop acceleration technique relies on the following notions of invariants. Here, “$\forall\mathcal{V}(\mathcal{T}).\ \psi$” abbreviates “$\forall(\mathcal{V}(\psi)\cap\mathcal{V}(\mathcal{T})).\ \psi$”, i.e., the quantifier binds all free variables of $\psi$ that occur in $\mathcal{T}$.

Definition 5** (Invariants).**

Let $\alpha\in\mathcal{T}$. If

[TABLE]

is valid, then $\varphi_{ci}$ is a conditional invariant of $\alpha$. If

[TABLE]

is valid, then $\varphi_{si}$ is a simple (conditional) invariant of $\alpha$. If $\varphi_{si}$ is a simple invariant of $\alpha$ and

[TABLE]

is valid, then $\varphi_{md}$ is monotonically decreasing for $\varphi_{si}$ and $\alpha$.

Recall that $\varphi$ is a (standard) invariant of a transition $\alpha$ if $\varphi$ holds whenever $\alpha$ is applied in a program run. If such a standard invariant $\varphi$ satisfies (ci), then $\varphi$ is usually called inductive. In contrast to inductive invariants, a conditional invariant $\varphi_{ci}$ does not have to hold when the control flow reaches $\alpha$, but if it does, then $\varphi_{ci}$ still holds after applying $\alpha$. Conditional invariants (resp. similar notions) are also used in, e.g., [40, 31, 32, 5, 9]. Monotonic decreasingness is converse to invariance: $\varphi_{md}$ is preserved when the effect of $\operatorname{up}_{\alpha}$ is undone.

We call constraints of the form $\varphi_{ci}\mathrel{\land}\varphi_{si}\mathrel{\land}\varphi_{md}$ monotonic if $\varphi_{ci}$ and $\varphi_{si}$ are conditional and simple invariants, and $\varphi_{md}$ is monotonically decreasing for $\varphi_{si}$. The reason is that the characteristic function \left\llbracket\varphi\right\rrbracket with \left\llbracket\varphi\right\rrbracket=1\iff\varphi and \left\llbracket\varphi\right\rrbracket=0\iff\neg\varphi of conditional invariants like $\varphi_{ci}$ and $\varphi_{si}$ is monotonically increasing w.r.t. $\operatorname{up}_{\alpha}$ and (md) essentially requires that \left\llbracket\varphi_{md}\right\rrbracket is monotonically decreasing w.r.t. $\operatorname{up}_{\alpha}$.

Example 6** (Invariants).**

For $\alpha_{2}$ from Ex. 1, $y\geq 0$ is a simple invariant and $x\geq 0$ is monotonically decreasing for $y\geq 0$, as

[TABLE]

are valid. Thus, $y\geq 0$ is also a conditional invariant. Note that it is not a standard invariant as there are program runs where $y\geq 0$ is violated when $\alpha_{2}$ is applied.

III-B Loop Acceleration

The key idea of loop acceleration for a simple loop, i.e., a transition $\alpha$ with $\operatorname{src}_{\alpha}=\operatorname{dest}_{\alpha}$, is to generate a new transition $\overline{\alpha}$ that captures $\mathit{k}$ iterations of $\alpha$. Here, $\mathit{k}$ is a fresh variable whose value can be chosen non-deterministically. We first use recurrence solving to compute closed forms for the values of the program variables after a symbolic number of iterations, i.e., a closed form of $\operatorname{up}_{\alpha}^{\mathit{k}}=\underbrace{\operatorname{up}_{\alpha}\circ\ldots\circ\operatorname{up}_{\alpha}}_{\mathit{k}\text{ times}}$. Then, as in [30], we exploit the following observation: If $\operatorname{guard}_{\alpha}$ holds after $\mathit{k}-1$ loop iterations and $\operatorname{up}_{\alpha}(\operatorname{guard}_{\alpha})$ implies $\operatorname{guard}_{\alpha}$ (i.e., $\operatorname{guard}_{\alpha}$ is monotonically decreasing), then $\operatorname{guard}_{\alpha}$ also holds after $\mathit{k}-2,\mathit{k}-3,\ldots,0$ iterations. Thus, adding $\operatorname{up}_{\alpha}^{\mathit{k}-1}(\operatorname{guard}_{\alpha})$ to $\operatorname{guard}_{\overline{\alpha}}$ ensures that $\mathit{k}$ only takes feasible values: If $\sigma$ satisfies $\operatorname{up}_{\alpha}^{\mathit{k}-1}(\operatorname{guard}_{\alpha})$, then $\alpha$ can be iterated at least $\sigma(\mathit{k})$ times.

However, $\operatorname{up}_{\alpha}(\operatorname{guard}_{\alpha})\Longrightarrow\operatorname{guard}_{\alpha}$ is rarely valid if $\operatorname{guard}_{\alpha}$ contains invariants of $\alpha$. Thus, our novel loop acceleration technique only requires monotonicity of $\operatorname{guard}_{\alpha}$ instead.

Theorem 7** (Accelerate).**

Let $\mathcal{T}$ be well formed, let $\alpha\in\mathcal{T}$ be a simple loop with $\operatorname{lhs}_{\alpha}=\mathsf{f}(\bm{x})$, let $\mathit{k}\in\mathcal{V}$ be fresh, and let $\mu$ be a substitution such that $\mu(\bm{x})=\operatorname{up}_{\alpha}^{\mathit{k}}(\bm{x})$ holds for all $\mathit{k}>0$. Moreover, let $\operatorname{guard}_{\alpha}=\varphi_{ci}\mathrel{\land}\varphi_{si}\mathrel{\land}\varphi_{md}$ be monotonic. Finally, let $\operatorname{dec}_{\mathit{k}}=\{\mathit{k}\mapsto\mathit{k}-1\}$ and $\overline{\mathcal{T}}=\mathcal{T}\cup\{\overline{\alpha}\}$ where

[TABLE]

Then the processor Accelerate: $\mathcal{T}\mapsto\overline{\mathcal{T}}$ is safe and sound.

So to construct $\operatorname{rhs}_{\overline{\alpha}}$, we compute a closed form $\mu$ that expresses $\mathit{k}$ iterations of the loop body as in [21, 30]. To do so, one can use state-of-the-art recurrence solvers like [1, 41, 27] to solve the system of recurrence relations $\bm{x}^{(\mathit{k}+1)}=\operatorname{up}_{\alpha}(\bm{x}^{(\mathit{k})})$ with the initial condition $\bm{x}^{(1)}=\operatorname{up}_{\alpha}(\bm{x})$.

To see why Accelerate is sound, assume that $\operatorname{guard}_{\overline{\alpha}}$ holds. As444In the following, we identify conjunctions and sets of inequations. $\varphi_{si}\subseteq\operatorname{guard}_{\overline{\alpha}}$ and $\varphi_{si}$ implies $\operatorname{up}_{\alpha}(\varphi_{si})$ by (si), we obtain

[TABLE]

Thus, as $\operatorname{guard}_{\overline{\alpha}}$ contains $\operatorname{dec}_{\mathit{k}}(\mu(\varphi_{md}))=\operatorname{up}_{\alpha}^{\mathit{k}-1}(\varphi_{md})$ and $\varphi_{si}\mathrel{\land}\operatorname{up}_{\alpha}(\varphi_{md})$ implies $\varphi_{md}$ by (md), we get

[TABLE]

So (1) and (2) imply $\varphi_{si}\mathrel{\land}\varphi_{md}$. As $\varphi_{ci}\subseteq\operatorname{guard}_{\overline{\alpha}}$ and $\operatorname{guard}_{\alpha}=\varphi_{ci}\mathrel{\land}\varphi_{si}\mathrel{\land}\varphi_{md}$, this means that $\operatorname{guard}_{\alpha}$ holds as well. As $\operatorname{guard}_{\alpha}$ implies $\operatorname{up}_{\alpha}(\varphi_{ci})$ (since $\varphi_{ci}\subseteq\operatorname{guard}_{\alpha}$ and $\varphi_{ci}$ is a conditional invariant), we obtain that $\operatorname{up}_{\alpha}(\varphi_{ci})$ holds. Together with (1) and (2) this means that $\operatorname{up}_{\alpha}(\operatorname{guard}_{\alpha})$ holds (if $1<\mathit{k}$). This in turn implies $\operatorname{up}_{\alpha}^{2}(\varphi_{ci})$, etc. Thus, we get

[TABLE]

Due to (1) – (3), the constraint $\varphi_{ci}\mathrel{\land}\varphi_{si}\mathrel{\land}\operatorname{dec}_{\mathit{k}}(\mu(\varphi_{md}))$ ensures that $\operatorname{guard}_{\alpha}=\varphi_{ci}\mathrel{\land}\varphi_{si}\mathrel{\land}\varphi_{md}$ holds before the $1^{st},\ldots,\mathit{k}^{th}$ iteration, as desired. Hence, every evaluation with $\overline{\alpha}$ can be replaced by $\mathit{k}$ evaluation steps with $\alpha$. Since $\operatorname{guard}_{\overline{\alpha}}$ enforces $\mathit{k}>0$, every non-terminating run with $\overline{\mathcal{T}}$ can therefore be transformed into a non-terminating run of $\mathcal{T}$.

Example 8** (Ex. 1 continued).**

Consider the simple loop $\alpha_{2}$ of Ex. 1. As $x\geq 0$ is not monotonic, Accelerate is not applicable. But if we strengthen the guard by adding the simple invariant $y\geq 0$, then $x\geq 0$ satisfies (md), cf. Ex. 6. Thus, we can apply Accelerate with $\varphi_{ci}:\;\mathsf{true}$, $\varphi_{si}:\;y\geq 0$, and $\varphi_{md}:\;x\geq 0$. Sect. IV will show how to find simple invariants like $y\geq 0$.

To compute a substitution $\mu$ that represents $k$ repeated updates, we solve the recurrence relations $y^{(\mathit{k}+1)}=y^{(\mathit{k})}+1$ and $x^{(\mathit{k}+1)}=x^{(\mathit{k})}-y^{(\mathit{k})}$ with the initial conditions $x^{(1)}=x-y$ and $y^{(1)}=y+1$, resulting in the solutions $y^{(\mathit{k})}=y+\mathit{k}$ and $x^{(\mathit{k})}=x-y\cdot\mathit{k}-\frac{1}{2}\cdot\mathit{k}^{2}+\frac{1}{2}\cdot\mathit{k}$, i.e., $\mu=\{x\mapsto x-y\cdot\mathit{k}-\frac{1}{2}\cdot\mathit{k}^{2}+\frac{1}{2}\cdot\mathit{k},\;y\mapsto y+\mathit{k}\}$. Thus, we accelerate $\alpha_{2}$ to

[TABLE]

for $\eta:\;\underbrace{y\geq 0}_{\varphi_{si}}\mathrel{\land}\operatorname{dec}_{\mathit{k}}(\mu(\varphi_{md}))\mathrel{\land}\mathit{k}>0$ where $\operatorname{dec}_{\mathit{k}}(\mu(\varphi_{md}))$ is $x-y\cdot(\mathit{k}-1)-\tfrac{1}{2}\cdot(\mathit{k}-1)^{2}+\tfrac{1}{2}\cdot(\mathit{k}-1)\geq 0.$

III-C Chaining

Accelerate only applies to simple loops. To transform loops with complex control flow into simple loops and to eventually obtain simplified programs, we use chaining, a standard technique to combine two transitions $\mathsf{f}(\ldots)\to\mathsf{g}(\ldots)$ and $\mathsf{g}(\ldots)\to\mathsf{h}(\ldots)$ to a new transition $\mathsf{f}(\ldots)\to\mathsf{h}(\ldots)$ that captures the effect of both transitions after each other.

Theorem 9** (Chain).**

Let $\mathcal{T}$ be well formed and let $\alpha,\beta\in\mathcal{T}$ where $\operatorname{dest}_{\alpha}=\operatorname{src}_{\beta}$, the argument lists of $\operatorname{lhs}_{\alpha}$ and $\operatorname{lhs}_{\beta}$ are equal, and $\mathcal{V}(\alpha)\cap\mathcal{V}(\beta)=\mathcal{V}(\operatorname{lhs}_{\alpha})$.555Otherwise, one can rename variables without affecting the relation ${\to_{\mathcal{T}}}$. Let $\mathcal{T}^{\circ}=\mathcal{T}\cup\{\alpha\circ\beta\}$ with

[TABLE]

Then the processor $\textbf{Chain}:\mathcal{T}\mapsto\mathcal{T}^{\circ}$ is safe and sound.

Chaining is not only useful to transform complex into simple loops, but it can also be used to combine a simple loop $\alpha$ with itself in order to enable loop acceleration and to obtain better closed forms for $\operatorname{up}_{\alpha}^{\mathit{k}}$. For example, consider the following loop, where the sign of $x$ alternates:

[TABLE]

The closed form $(-1)^{\mathit{k}}\cdot x$ for the value of $x$ after $\mathit{k}$ iterations involves exponentials even though $x$ does not grow exponentially. This is disadvantageous, as our implementation relies on SMT solving, but SMT solvers have limited support for non-polynomial arithmetic. Moreover, Accelerate is not applicable, as $y>x$ is non-monotonic. However, this can be resolved by chaining $\alpha_{neg}$ with itself, which results in

[TABLE]

This transition can be accelerated to

[TABLE]

where $\operatorname{dec}_{\mathit{k}}(\mu(\operatorname{guard}_{\alpha_{neg}\circ\alpha_{neg}}))$ is

[TABLE]

i.e., the accelerated transition does not contain exponentials.

So for simple loops $\alpha$ that alternate the sign of a variable (i.e., where $\operatorname{up}_{\alpha}(x)=c\cdot x+t$ for some $x\in\mathcal{V}(\operatorname{lhs}_{\alpha})$, $c<0$, and $t\in\mathcal{A}$ with $x\notin\mathcal{V}(t)$), we accelerate $\alpha\circ\alpha$ instead of $\alpha$.

Chaining can also help to obtain simpler closed forms for transitions where variables are set to constants. For example, a closed form for the repeated update of the variable $z$ in

[TABLE]

is $0^{\mathit{k}-1}\cdot y+(1-0^{\mathit{k}-1})\cdot 2$, which is again not polynomial. However, chaining $\alpha_{const}$ with itself yields

[TABLE]

(where we simplified the guard), which can be accelerated to

[TABLE]

i.e., the accelerated transition again only contains polynomials.

Finally, chaining can also make acceleration applicable to loops that permute arguments:

[TABLE]

While $\alpha_{p}$ violates the prerequisites of Accelerate,

[TABLE]

can be accelerated to:

[TABLE]

So to handle simple loops $\alpha$ where some variables “stabilize” (i.e., $\operatorname{up}_{\alpha}^{n}(z)\in\mathbb{Z}$ for some $z\in\mathcal{V}$ and some $n>1$, as in $\alpha_{const}$) or where arguments are permuted (as in $\alpha_{p}$), we repeatedly chain $\alpha$ with itself as long as this reduces the size of

[TABLE]

III-D Proving Non-Termination

To detect non-terminating simple loops $\alpha$, we check whether $\operatorname{guard}_{\alpha}$ itself is a simple invariant (i.e., whether the valuations that satisfy $\operatorname{guard}_{\alpha}$ correspond to a recurrent set of the relation ${\to_{\{\alpha\}}}$, cf. [26]).

Theorem 10** (Nonterm).**

Let $\mathcal{T}$ be well formed and let $\alpha\in\mathcal{T}$ be a simple loop such that $\operatorname{guard}_{\alpha}$ is a simple invariant. Moreover, let $\mathcal{T}^{\omega}=\mathcal{T}\cup\{\alpha^{\omega}\}$ where

[TABLE]

Then the processor $\textbf{Nonterm}:\mathcal{T}\mapsto\mathcal{T}^{\omega}$ is safe and sound.

Example 11** (Ex. 1 continued).**

Clearly, $y>0$ is not a simple invariant of $\alpha_{4}$ from Ex. 1. But if we strengthen the guard by adding the simple invariant $x\leq 0$, then Nonterm is applicable as $y>0\mathrel{\land}x\leq 0$ implies $y-x>0\mathrel{\land}x\leq 0$. Thus, we obtain

[TABLE]

Again, we will see how to deduce suitable simple invariants like $x\leq 0$ automatically in Sect. IV.

In some cases, chaining also helps to make Nonterm applicable. To see this, consider the simple loop

[TABLE]

where $y>0$ is no simple invariant. Chaining it with itself yields

[TABLE]

As $y>0\mathrel{\land}y-x>0\implies y-x>0\mathrel{\land}y-x-0>0$ is valid, the prerequisites of Nonterm are satisfied and we obtain

[TABLE]

So in general, we try to apply Nonterm not only to a simple loop $\alpha$, but also to $\alpha\circ\alpha$. Apart from Nonterm, we also use SMT solving to check whether a loop has a fixpoint, which is a standard technique to prove non-termination.

Theorem 12** (Fixpoint).**

Let $\mathcal{T}$ be well formed, let $\alpha\in\mathcal{T}$ be a simple loop with $\operatorname{lhs}_{\alpha}=\mathsf{f}(\bm{x})$, and let $\operatorname{guard}_{\alpha}\mathrel{\land}\bm{x}=\operatorname{up}_{\alpha}(\bm{x})$ be satisfiable. Let $\mathcal{T}^{\bm{f\!p}}=\mathcal{T}\cup\{\alpha^{\bm{f\!p}}\}$ where

[TABLE]

Then the processor $\textbf{Fixpoint}:\mathcal{T}\mapsto\mathcal{T}^{\bm{f\!p}}$ is safe and sound.

For example, $\{x\mapsto 0,y\mapsto 1\}$ is a fixpoint of $\alpha_{nt}$ which satisfies $y>0$ and $(x,y)=(0,y-x)$ (i.e., $x=0\mathrel{\land}y=y-x$).

Procedure 1 shows a streamlined version of the strategy that we use to apply the presented processors. It combines chaining, loop acceleration, and our non-termination processors to transform arbitrary programs into simplified programs. For nested loops, the elimination starts with the inner loops. Note that deleting transitions (Steps 1, 1, 1, and 1) is always sound in our setting.

We present the algorithm $\operatorname{\mathbf{deduceInvariants}}$ for Step 1 in Sect. IV. It creates variants of $\alpha$ by extending $\operatorname{guard}_{\alpha}$ with suitable constraints to make Accelerate or Nonterm applicable. Step 1 chains $\alpha$ with all preceding transitions that are no simple loops. Steps 1 and 1 eliminate a function symbol via chaining. Note that Procedure 1 could have non-terminating runs, as it may add new transitions in Step 1. However, this turned out to be unproblematic in our experiments, cf. Sect. V.

Example 13** (Ex. 1 finished).**

After accelerating $\alpha_{2}$ in Step 1 (see Ex. 8), Procedure 1 computes

[TABLE]

in Step 1 where $\eta$ is

[TABLE]

Next, it applies Nonterm to $\alpha_{4}$ in Step 1 (see Ex. 11) and chains the resulting transition with $\alpha_{3}$ in Step 1, which yields

[TABLE]

Then, it chains $\alpha_{1}\circ\overline{\alpha}_{2}$ and $\alpha_{3}\circ\alpha_{4}^{\omega}$ in Step 1, resulting in

[TABLE]

where $\psi$ is $\eta\mathrel{\land}\underbrace{x-y\cdot\mathit{k}-\tfrac{1}{2}\cdot\mathit{k}^{2}+\tfrac{1}{2}\cdot\mathit{k}<0}_{\operatorname{up}_{\alpha_{1}\circ\overline{\alpha}_{2}}(x<0)}\mathrel{\land}\underbrace{y+\mathit{k}>0}_{\operatorname{up}_{\alpha_{1}\circ\overline{\alpha}_{2}}(y>0)}$.

To prove non-termination, we have to show satisfiability of $\psi$. As $\sigma\models\psi$ for $\sigma=\{x\mapsto 0,y\mapsto 0,\mathit{k}\mapsto 2\}$, the configuration $\sigma(\mathsf{start}(x,y))=\mathsf{start}(0,0)$ witnesses non-termination of Ex. 1.

So loop acceleration introduces a new variable $\mathit{k}$ for the number of loop unrollings. Later, $\mathit{k}$ is instantiated when searching for models of the guards of the simplified transitions which result from repeated acceleration and chaining. In Ex. 13, when inferring a model for the guard of $\alpha_{1}\circ\overline{\alpha}_{2}\circ\alpha_{3}\circ\alpha_{4}^{\omega}$, the instantiation $\mathit{k}\mapsto 2$ means that $\alpha_{2}$ is applied twice in the corresponding non-terminating run of the original program.

IV Deducing Simple Invariants

In Sect. III, we have seen that we sometimes need to deduce suitable simple invariants to apply our novel loop acceleration technique or to prove non-termination. Soundness of adding constraints to transitions is ensured by the following processor.

Theorem 14** (Strengthen [21]).**

Let $\mathcal{T}$ be well formed, let $\alpha\in\mathcal{T}$, let $\varphi$ be a constraint, and let $\mathcal{T}^{\bullet}=\mathcal{T}\cup\{\alpha^{\bullet}\}$ where

[TABLE]

Then the processor $\textbf{Strengthen}:\mathcal{T}\mapsto\mathcal{T}^{\bullet}$ is safe and sound.

The challenge is to find constraints $\varphi$ that help to prove non-termination. We now explain how to automatically synthesize suitable simple invariants to strengthen a simple loop $\alpha$, cf. Contribution (b) from Sect. I. Our approach iteratively generates simple invariants such that larger and larger parts of $\operatorname{guard}_{\alpha}$ become monotonic. To this end, it constructs arithmetic formulas and uses constraint solvers to instantiate their free variables (or parameters) such that they become valid. This results in simple invariants that are suitable for strengthening. Eventually, our technique either fails to synthesize further invariants or the whole guard becomes monotonic, so that we can apply Accelerate or even Nonterm (if $\alpha$’s guard is a simple invariant).

To synthesize simple invariants, we first compute a maximal subset $\varphi_{i}$ of $\operatorname{guard}_{\alpha}$ such that $\varphi_{i}$ is a conditional invariant. However, to apply Accelerate, not all constraints of $\operatorname{guard}_{\alpha}$ need to be conditional invariants, as long as the remaining constraints are monotonically decreasing. Hence, we next compute a maximal subset $\varphi_{si}$ of $\varphi_{i}$ such that $\varphi_{si}$ is a simple invariant. Then we can determine a maximal subset $\varphi_{md}$ of $\operatorname{guard}_{\alpha}\setminus\,\varphi_{i}$ which is monotonically decreasing for $\varphi_{si}$.

IV-A Generating New Invariants

Let the set of parameters $\mathcal{P}\subset\mathcal{V}$ be countably infinite and disjoint from the program variables $\mathcal{V}(\mathcal{T})$. Moreover, let $\varphi_{nm}=\operatorname{guard}_{\alpha}\setminus\;(\varphi_{i}\cup\varphi_{md})$, i.e., $\varphi_{nm}$ causes non-monotonicity of $\operatorname{guard}_{\alpha}$. For each inequation $\rho\in\varphi_{nm}$, we construct a linear template $\operatorname{\tau}_{\rho}$ over the relevant variables $\mathcal{V}_{\rho}$ of $\rho$, i.e., $\mathcal{V}_{\rho}$ is the smallest set such that $\mathcal{V}(\rho)\subseteq\mathcal{V}_{\rho}$, $\mathcal{V}(\rho^{\prime})\cap\mathcal{V}_{\rho}\neq\varnothing$ implies $\mathcal{V}(\rho^{\prime})\subseteq\mathcal{V}_{\rho}$ for each $\rho^{\prime}\in\operatorname{guard}_{\alpha}$, and $x\in\mathcal{V}_{\rho}$ implies $\mathcal{V}(\operatorname{up}_{\alpha}(x))\subseteq\mathcal{V}_{\rho}$. So $\operatorname{\tau}_{\rho}$ has the form $\sum_{x\in\mathcal{V}_{\rho}}c_{x}\cdot x\geq c$ where $\{c_{x}\mid x\in\mathcal{V}_{\rho}\}\cup\{c\}\subset\mathcal{P}$.

For $\alpha_{4}$ from Ex. 1, we obtain $\varphi_{i}=\varnothing$, $\varphi_{md}=\varnothing$, and $\varphi_{nm}=\{y>0\}$. As $x\in\operatorname{up}_{\alpha_{4}}(y)$, we have $\mathcal{V}_{y>0}=\{x,y\}$. Hence, $\operatorname{\tau}_{y>0}$ is $c_{x}\cdot x+c_{y}\cdot y\geq c$ where $c_{x},c_{y},c\in\mathcal{P}$.

To find a valuation of the parameters such that all templates can be added to $\varphi_{si}$ without violating the definition of simple invariants, we enforce (si) for $\varphi_{si}\mathrel{\land}\bigwedge_{\rho\in\varphi_{nm}}\operatorname{\tau}_{\rho}$ by requiring

[TABLE]

So for $\alpha_{4}$, we search for a valuation of $c_{x},c_{y},$ and $c$ that satisfies

[TABLE]

IV-B Improving Towards Monotonicity

By construction, the constraint $\varphi_{i}\mathrel{\land}\varphi_{md}$ is monotonic. Furthermore, ($\tau$-si) ensures that $\varphi_{si}\mathrel{\land}\bigwedge_{\rho\in\varphi_{nm}}\operatorname{\tau}_{\rho}$ is a simple invariant, i.e., we know that

[TABLE]

is monotonic. Eventually, our goal is to turn $\operatorname{guard}_{\alpha}$ into a simple invariant and apply Nonterm or to make it monotonic and apply Accelerate. To progress towards this goal incrementally, we ensure that we can add at least one $\rho\in\varphi_{nm}$ to (5) without violating monotonicity. To this end, we enforce that (ci) or (md) holds for some $\rho\in\varphi_{nm}$ by requiring:

[TABLE]

Note that (some-ci) can also help to apply Nonterm as $\operatorname{guard}_{\alpha}$ is a conditional invariant iff it is a simple invariant.

IV-C Maximizing the Improvement

It is clearly advantageous to instantiate the parameters in such a way that as many inequations from $\varphi_{nm}$ as possible can be added to (5) without violating monotonicity. Hence, we require

[TABLE]

for as many $\rho\in\varphi_{nm}$ as possible, i.e., each $\rho\in\varphi_{nm}$ gives rise to a soft requirement $\eqref{eq:inv-soft}\lor\eqref{eq:inv-soft-decreasing}$. Later, soft requirements will be associated with weights. We then try to maximize the weight of all valid soft requirements, but some of them may be violated. However, all hard requirements like ($\tau$-si) and $\eqref{eq:inv-psi-invariant}\vee\eqref{eq:inv-psi-decreasing}$ must hold.

For $\alpha_{4}$, $\varphi_{nm}$ is a singleton set and hence (some-ci) and ($\rho$-ci) resp. (some-md) and ($\rho$-md) coincide for $\rho:\;y>0$.

[TABLE]

IV-D Preferring Local Invariants

If we strengthen a transition $\alpha$ with an inequation $\xi$, then the case $\neg\xi$ is not covered by the resulting transition. So we split $\alpha$ relative to $\xi$, i.e., we also strengthen $\alpha$ with $\neg\xi$. However, this increases the size of the program. Thus, we try to deduce standard invariants whenever possible, i.e., we try to deduce constraints $\xi$ that are valid whenever $\alpha$ is applied in a program run so that the case $\neg\xi$ is irrelevant. To detect such invariants in a modular way, we only consider local invariants, i.e., constraints whose invariance can be proven by reasoning about $\alpha$ and all transitions $\beta$ with $\operatorname{dest}_{\beta}=\operatorname{src}_{\alpha}$, whereas all other transitions are ignored. A similar idea is also used in [32] to synthesize invariants.

Definition 15** (Local Invariants).**

Let $\alpha\in\mathcal{T}$. If $\varphi_{li}$ is a conditional invariant of $\alpha$ and for all $\beta\in\mathcal{T}\setminus\{\alpha\}$ with $\operatorname{dest}_{\beta}=\operatorname{src}_{\alpha}$,

[TABLE]

is valid, then $\varphi_{li}$ is a local invariant of $\alpha$.

Def. 15 requires that whenever $\beta$ can be applied ($\operatorname{guard}_{\beta}$ in the premise of (li)) and $\alpha$ can be applied afterwards ($\operatorname{dest}_{\beta}=\operatorname{src}_{\alpha}$ and $\operatorname{up}_{\beta}(\operatorname{guard}_{\alpha})$ in the premise of (li)), then $\varphi_{li}$ must hold after applying $\beta$ (which is the conclusion of (li)).

So for $\alpha_{4}$, $x\leq 0$ is clearly a simple invariant, as $\alpha_{4}$ does not update $x$. Moreover, the guard $x<0$ of $\alpha_{3}$ (which is the only other transition whose destination is $\operatorname{src}_{\alpha_{4}}$) implies $x\leq 0$. Thus, $x\leq 0$ is a local invariant of $\alpha_{4}$.

To guide the search towards local invariants, we add a soft requirement corresponding to (li) for each $\rho\in\varphi_{nm}$:

[TABLE]

So for $\rho:\,y>0$ in our example, due to transition $\alpha_{3}$ we get:

[TABLE]

IV-E Excluding Inapplicable Transitions

So far we do not exclude solutions that result in inapplicable transitions. To solve this problem, we add the hard requirement

[TABLE]

So we require that there is a transition $\beta$ with $\operatorname{dest}_{\beta}=\operatorname{src}_{\alpha}$ (due to the leading $\bigvee\ldots$) and a valuation (due to the existential quantifier) such that $\beta$ is applicable (due to $\operatorname{guard}_{\beta}$) and $\alpha$ is applicable afterwards (due to $\operatorname{up}_{\beta}(\operatorname{guard}_{\alpha})\mathrel{\land}\bigwedge_{\rho\in\varphi_{nm}}\operatorname{up}_{\beta}(\operatorname{\tau}_{\rho})$, as we will strengthen $\alpha$’s guard with $\bigwedge_{\rho\in\varphi_{nm}}\operatorname{\tau}_{\rho}$ after instantiating the parameters in the templates). Thus, for $\alpha_{4}$ we require

[TABLE]

due to the transition $\alpha_{3}$.

Procedure 1 essentially compresses each path through a multi-path loop (e.g., a loop whose body contains case analyses) into a simple loop via chaining in order to apply Nonterm, Fixpoint, or Accelerate afterwards. So our technique tends to generate many simple loops for function symbols that correspond to entry points of multi-path loops. Therefore, ($\operatorname{\tau}_{\rho}$-li) and (sat) can result in large formulas, which leads to performance issues. Hence, our implementation only considers transitions $\beta$ with $\operatorname{src}_{\beta}\neq\operatorname{dest}_{\beta}$ when constructing ($\operatorname{\tau}_{\rho}$-li) and (sat). Note that this is uncritical for correctness, as the technique presented in the current section is only a heuristic to generate constraints to be added via Strengthen (which is always sound).

IV-F *Preferring *Nonterm

Finally, we prefer simple invariants that allow us to apply Nonterm, our main technique to prove non-termination. To this end, we add a soft requirement to prefer solutions where the guard of the resulting strengthened transition is a conditional invariant whenever $\varphi_{md}$ is empty:

[TABLE]

In our example, (nt) equals ($\rho$-ci-$\alpha_{4}$) as $\varphi_{nm}$ is a singleton set.

IV-G Algorithm for Inferring Simple Invariants

Procedure 2 summarizes our approach to deduce simple invariants. Here, the $i^{th}$ entry of the weight vector $\bm{w}$ corresponds to the weight of the $i^{th}$ soft requirement $\chi_{i}$ and $\operatorname{\mathbf{solve}}(\zeta,\bm{\chi},\bm{w})$ searches an instantiation $\sigma$ of the parameters such that $\sigma\models\zeta$ and $\sum_{\begin{subarray}{c}1\leq i\leq|\bm{\chi}|\\ \sigma\models\chi_{i}\end{subarray}}w_{i}$ is maximized. We explain how to implement $\operatorname{\mathbf{solve}}$ in Sect. IV-H. The weights are chosen in such a way that a solution $\sigma$ is preferred over $\sigma^{\prime}$ if $\sigma$ turns more templates $\operatorname{\tau}_{\rho}$ into local invariants than $\sigma^{\prime}$: The weight $m+2=|\varphi_{nm}|+2$ of the formulas resulting from ($\operatorname{\tau}_{\rho}$-li) (where $|\varphi_{nm}|$ is the number of inequations in $\varphi_{nm}$) ensures that each formula from $\eqref{eq:inv-standard}$ has a higher weight than the sum of all other soft requirements $\eqref{eq:inv-soft}\lor\eqref{eq:inv-soft-decreasing}$ and (nt).

Note that Step 2 updates $\operatorname{guard}_{\alpha}$ in each iteration and $\varphi_{nm}$ is recomputed before checking the condition of the while-loop in Step 2. Procedure 2 terminates: $|\varphi_{nm}|$ decreases in every iteration due to the hard requirement $\eqref{eq:inv-psi-invariant}\lor\eqref{eq:inv-psi-decreasing}$, which ensures that some $\rho\in\varphi_{nm}$ becomes part of $\varphi_{i}$ or $\varphi_{md}$. Moreover, the hard requirement ($\tau$-si) ensures that each $\sigma(\operatorname{\tau}_{\rho})$ becomes part of $\varphi_{si}$, so Procedure 2 never adds elements to $\varphi_{nm}$.

In our example, ($\tau$-si-$\alpha_{4}$), ($\rho$-ci-$\alpha_{4}$), ($\operatorname{\tau}_{\rho}$-li-$\alpha_{4}$), and (sat-$\alpha_{4}$) are valid if $c_{x}=-1$ and $c_{y}=c=0$. Hence, Procedure 2 successfully generates the local invariant $-x\geq 0$, i.e., $x\leq 0$. Afterwards, we can apply Nonterm to the strengthened loop as in Ex. 11.

Example 16** (Deducing Simple Invariants for $\alpha_{2}$).**

Reconsider the simple loop $\alpha_{2}$ from Ex. 1, where $\varphi_{i}=\varphi_{md}=\varnothing$ and $\varphi_{nm}=\{x\geq 0\}$ as $\alpha_{2}$’s guard $x\geq 0$ is not monotonic. Here, $\operatorname{\tau}_{x\geq 0}$ is $c_{x}\cdot x+c_{y}\cdot y\geq c$ as $y\in\mathcal{V}(\operatorname{up}_{\alpha}(x))$. So ($\tau$-si) becomes

[TABLE]

*Again, $\eqref{eq:inv-psi-invariant}\lor\eqref{eq:inv-psi-decreasing}$ coincides with $\eqref{eq:inv-soft}\lor\eqref{eq:inv-soft-decreasing}$ for $\rho:\,x\geq 0$.

$\displaystyle\forall x,y.\ x\geq 0\mathrel{\land}c_{x}\cdot x+c_{y}\cdot y\geq c\implies x-y\geq 0\hskip 5.0pt\lor$

($\rho$-ci-$\alpha_{2}$)

$\displaystyle\forall x,y.\ c_{x}\cdot x+c_{y}\cdot y\geq c\mathrel{\land}x-y\geq 0\implies x\geq 0$

($\rho$-md-$\alpha_{2}$)

Next, ($\operatorname{\tau}_{\rho}$-li) gives rise to the requirement*

[TABLE]

Moreover, (sat) becomes

[TABLE]

Finally, (nt) equals ($\rho$-ci-$\alpha_{2}$). Thus, the hard requirement $\zeta$ is

[TABLE]

The soft requirements are ($\tau_{\rho}$-li-$\alpha_{2}$), $\eqref{eq:inv-increasing-ex}\lor\eqref{eq:inv-decreasing-ex}$, and ($\rho$-ci-$\alpha_{2}$) with weights $3$, $1$, and $1$, respectively. The valuation $\sigma=\{c_{x}\mapsto 0,c_{y}\mapsto 1,c\mapsto 0\}$ satisfies $\zeta$ and $\eqref{eq:inv-increasing-ex}\lor\eqref{eq:inv-decreasing-ex}$, but not the other soft constraints. As $\zeta\mathrel{\land}\eqref{eq:inv-standard-decreasing-ex}$ and $\zeta\mathrel{\land}\eqref{eq:inv-increasing-ex}$ are unsatisfiable, $\sigma$ is an optimal solution. It corresponds to the simple invariant $y\geq 0$. After deducing it, the strengthened transition can be accelerated as in Ex. 8.

IV-H Greedy Algorithm for Max-SMT Solving

We now explain how to implement the function $\operatorname{\mathbf{solve}}$ that is called in Procedure 2 to instantiate the parameters in the formulas. Our implementation is restricted to the case that these formulas are linear w.r.t. the program variables $\mathcal{V}(\mathcal{T})$. Then the universally quantified variables can be eliminated by applying Farkas’ Lemma [6, 36]. In this way, we obtain a Max-SMT obligation over the theory of non-linear integer666Note that rational constants can be eliminated by multiplying with the least common multiple. arithmetic. While there exist powerful Max-SMT solvers [15, 4, 18], we use a straightforward greedy algorithm based on incremental SMT solving. This approach turned out to be be more efficient than sophisticated Max-SMT techniques in our setting, presumably as it does not aim to find provably optimal solutions.

V Experiments

We implemented our approach in our tool LoAT [21] which uses the recurrence solver PURRS [1] and the SMT solver Z3 [15]. It supports the SMT-LIB input format [8] and the native formats of the tools KoAT [10] and T2 [11]. We evaluated it on the benchmark suite from the Termination and Complexity Competition (TermComp [23]) consisting of 1222 programs (TPDB [38], category Termination of Integer Transition Systems). All experiments were executed on StarExec [37] with a timeout of 60 seconds per example.

We first compared our new implementation with our technique to prove lower complexity bounds of integer programs from [21] (LoAT LB), which can also deduce non-termination as a byproduct. LoAT LB proves non-termination in 390 cases, whereas the new version of LoAT succeeds for 462 examples.

Then, we compared LoAT with two state-of-the-art termination analyzers for integer programs: VeryMax [5, 32] (resp. its predecessor CppInv) won the category Termination of Integer Transition Systems at TermComp in 2014 and 2016 – 2019. T2 was the winner in 2015. We also tested with our tool AProVE [22], but excluded it as it uses a similar approach like T2, but finds fewer non-termination proofs. The remaining participants of the respective category of TermComp, Ctrl [29] and iRankFinder [2, 16], cannot prove non-termination.777iRankFinder can prove non-termination of simple loops [2], but according to its authors it cannot yet check reachability of diverging configurations. We used the TermComp ’19 version of VeryMax and the TermComp ’17 version of T2 (as T2 has not been developed further since 2017). Our experiments did not reveal any conflicts, i.e., there is no example where one tool proved termination and another proved non-termination.

[TABLE]

As the table above shows, LoAT proves non-termination more often than any other tool. According to the second last row, it solves 22 examples where all other tools fail. Together, T2 and all TermComp participants succeed on 1130 examples. So LoAT solves 23.9% of the 92 remaining potentially non-terminating examples.

The TPDB examples mostly use linear arithmetic and T2 and VeryMax are restricted to such programs [11, 32]. To evaluate LoAT on examples with non-linear arithmetic, we also compared with the tool Anant [14], which has been specifically designed to handle non-linearity. Here, we used the 29 non-terminating programs with non-linear arithmetic from the evaluation of [14]. As we were not able to run Anant, even though the authors kindly provided the source code and old binaries, we compared with the results presented in [14].

[TABLE]

Together, Anant and LoAT prove non-termination of all examples. LoAT solves one example less than Anant, but it is significantly faster: It always terminates within less than three seconds whereas Anant takes up to 4 minutes in some cases. However, both tools were run on different machines.

Finally, we compared LoAT with the tools from the category Termination of C Integer Programs at TermComp ’19888Ultimate and AProVE were also the two most powerful tools in the “termination” category for C programs at SV-COMP ’19 [3]. (AProVE [22], Ultimate [12], and VeryMax [5, 32]) on the 355 examples from that category of the TPDB. As LoAT cannot parse C, we coupled it with a version of AProVE that converts C programs into equivalent integer programs.

[TABLE]

The results of LoAT are competitive, but it succeeds on less examples than AProVE and VeryMax. VeryMax and LoAT are the only tools that find unique non-termination proofs. Finally, LoAT is the fastest tool, although its runtime includes AProVE’s conversion from C. However, all tools but LoAT also spend time on attempting to prove termination, which may explain their longer runtime.

To explain the discrepancy between the results for integer programs and for C programs, note that the integer programs from the TPDB often contain several loops. Here, our loop acceleration technique is particularly successful, because the challenge is not only to prove non-termination of one of the loops, but also to prove its reachability. In contrast, many C programs from the TPDB consist of a single multi-path loop. So to prove non-termination, one has to find a suitable pattern to execute the paths through the loop’s body. To improve the handling of such examples, we will extend our approach by control flow refinement techniques [25, 17, 20, 30] in future work.

See https://ffrohn.github.io/acceleration for a pre-compiled binary (Linux, 64 bit) of LoAT, tables with detailed results for all benchmarks, and the full output of the tools for all examples (the detailed results of Anant can be found in [14]). The source code of the implementation in our tool LoAT is available at https://github.com/aprove-developers/LoAT/tree/nonterm.

VI Conclusion and Related Work

VI-A Conclusion

We presented the first non-termination technique based on loop acceleration. It accelerates terminating loops in order to prove reachability of non-terminating configurations, even if this requires reasoning about program parts that contain loops themselves. As we use a non-termination criterion which is a special case of the prerequisites of our novel loop acceleration technique (see Sect. III), we can use the same new invariant inference technique (Sect. IV) to facilitate both loop acceleration and non-termination proving. The experimental evaluation of our approach shows that it is competitive with state-of-the-art tools, cf. Sect. V.

VI-B Related Work

Loop Acceleration is mostly used in over-approximating settings (e.g., [19, 24, 28, 35]), whereas our setting is under-approximating. We only know of two other under-approximating loop acceleration techniques [21, 30]: One requires metering functions [21], an adaption of ranking functions, that can be challenging to synthesize. The other [30] is a special case of Thm. 7 where $\varphi_{ci}=\varphi_{si}=\mathsf{true}$, which restricts its applicability in comparison to our approach. To facilitate acceleration, [30] splits disjunctive guards, which is orthogonal to our splitting of guards by adding conjuncts (cf. Sect. IV-D).

Most techniques to prove non-termination first generate lassos consisting of a simple loop $\alpha$ and a stem, i.e., a path from the program’s entry point to $\alpha$. Then they try to prove non-termination of these lassos. However, a program with consecutive or nested loops usually has infinitely many possible lassos. In contrast, our program simplification framework yields a loop-free simplified program with finitely many transitions.

In [26], recurrent sets were proposed to prove non-termination. A set of configurations is recurrent if each element has a successor in the set. Hence, a non-empty recurrent set that contains an initial configuration witnesses non-termination. There are many techniques to find recurrent sets for simple loops [2], lassos [26, 7, 13, 40], or more complex sub-programs [32]. Essentially, our invariant inference technique of Sect. IV also searches for a recurrent set for a simple loop $\alpha$. However, if it cannot find a recurrent set it may still successfully enforce monotonicity of $\operatorname{guard}_{\alpha}$ and hence allow us to accelerate $\alpha$.

An alternative to recurrent sets is presented in [34]. It represents infinite runs as sums of geometric series. In general, we could use any technique to prove non-termination of simple loops or lassos as an alternative to our non-termination criteria.

Further approaches to prove non-termination are, e.g., based on Hoare-style reasoning [33] or safety proving [39].

While most related techniques to prove non-termination focus on linear arithmetic, [14] has been specifically designed to handle non-linear arithmetic via live abstractions and a variation of recurrent sets. As shown in Sect. V, our approach is also competitive on programs with non-linear arithmetic.

VI-C Future Work

We will integrate control flow refinement techniques and more powerful non-termination criteria (e.g., to find disjunctive recurrent sets, which we cannot handle yet). We will also consider techniques to infer non-linear invariants, as our current invariant inference is restricted to linear arithmetic.

VI-D Acknowledgments

We thank Marc Brockschmidt and Matthias Naaf for important initial discussions.

Appendix A Proofs

A-A Proof of Thm. 7

Proof.

We first show that for any valuation $\sigma$, $\sigma\models\operatorname{guard}_{\overline{\alpha}}$ implies

[TABLE]

Let $\sigma$ be a valuation with $\sigma\models\operatorname{guard}_{\overline{\alpha}}$. As $\varphi_{si}$ is a simple invariant, $\varphi_{si}$ implies $\operatorname{up}_{\alpha}(\varphi_{si})$. Since $\varphi_{si}\subseteq\operatorname{guard}_{\overline{\alpha}}$, we obtain

[TABLE]

As we also have $\operatorname{dec}_{\mathit{k}}(\mu(\varphi_{md}))\subseteq\operatorname{guard}_{\overline{\alpha}}$, we get

[TABLE]

by definition of $\operatorname{dec}_{\mathit{k}}$ and $\mu$.

We now use induction on $m$ to prove

[TABLE]

The induction base $m=1$ is immediate due to (9). For the induction step, let $m>1$. Due to the induction hypothesis, we obtain

[TABLE]

By (md), we have

[TABLE]

Hence, (11) and (8) imply

[TABLE]

This finishes the proof of (10), which is equivalent to

[TABLE]

We now prove999Note that in contrast to the statement (8) for simple invariants, $\sigma\models\operatorname{up}_{\alpha}^{n}(\varphi_{ci})$ does not necessarily hold for all $n\in\mathbb{N}$. This is the reason why we distinguish between simple and conditional invariants and only use simple invariants in the premise of (md).

[TABLE]

by induction on $n$. For the induction base ($n=0$) we have $\sigma\models\varphi_{ci}$ since $\varphi_{ci}\subseteq\operatorname{guard}_{\overline{\alpha}}$. For the induction step, let $n>0$. Due to the induction hypothesis, we get

[TABLE]

Moreover, we have

[TABLE]

and

[TABLE]

due to (8) and (12). As $\operatorname{guard}_{\alpha}=\varphi_{ci}\mathrel{\land}\varphi_{si}\mathrel{\land}\varphi_{md}$, we obtain

[TABLE]

As $\varphi_{ci}$ is a conditional invariant and $\varphi_{ci}\subseteq\operatorname{guard}_{\alpha}$, $\operatorname{guard}_{\alpha}$ also implies $\operatorname{up}_{\alpha}(\varphi_{ci})$. Thus, we get

[TABLE]

This finishes the proof of (13).

Since, again, $\operatorname{guard}_{\alpha}=\varphi_{ci}\mathrel{\land}\varphi_{si}\mathrel{\land}\varphi_{md}$, (8), (12), and (13) together imply

[TABLE]

which finishes the proof of (7).

Thus, we have

[TABLE]

for any model $\sigma$ of $\operatorname{guard}_{\overline{\alpha}}$, where the evaluation takes $\sigma(\mathit{k})>0$ steps. As

[TABLE]

by the definition of $\mu$, this shows that any evaluation with $\overline{\alpha}$ can be replaced by at least one evaluation step with $\alpha$. Thus, every non-terminating evaluation with $\overline{\mathcal{T}}$ can be transformed into a corresponding non-terminating evaluation with $\mathcal{T}$. Hence, the processor Accelerate is sound.

The processor is also safe, i.e., $\overline{\mathcal{T}}$ is well formed. The reason is that by the argumentation above, if $\sigma$ is a valuation with $\sigma\models\operatorname{guard}_{\overline{\alpha}}$, then the configuration $\sigma(\operatorname{lhs}_{\overline{\alpha}})$ can be evaluated to $\sigma(\operatorname{rhs}_{\overline{\alpha}})$ with the well-formed program $\mathcal{T}$ and thus, $\sigma(\operatorname{rhs}_{\overline{\alpha}})$ must also be a configuration. ∎

A-B Proof of Thm. 9

Proof.

Let $\sigma$ be a model of $\operatorname{guard}_{\alpha}\mathrel{\land}\operatorname{up}_{\alpha}(\operatorname{guard}_{\beta})$ with $\mathcal{V}(\alpha)\cup\mathcal{V}(\beta)\subseteq\operatorname{dom}(\sigma)$. Then $\sigma\models\operatorname{guard}_{\alpha}$ implies $\sigma(\operatorname{lhs}_{\alpha})\to_{\mathcal{T}}\sigma(\operatorname{rhs}_{\alpha})=\sigma(\operatorname{up}_{\alpha}(\operatorname{lhs}_{\beta}))$, as $\operatorname{dest}_{\alpha}=\operatorname{src}_{\beta}$ and the argument lists of $\operatorname{lhs}_{\alpha}$ and $\operatorname{lhs}_{\beta}$ are equal. From $\sigma\models\operatorname{up}_{\alpha}(\operatorname{guard}_{\beta})$ and the fact that $\sigma\circ\operatorname{up}_{\alpha}$ is a valuation due to well-formedness of $\{\alpha\}$, we obtain $\sigma\circ\operatorname{up}_{\alpha}\models\operatorname{guard}_{\beta}$. Thus, we get $\sigma(\operatorname{up}_{\alpha}(\operatorname{lhs}_{\beta}))\to_{\mathcal{T}}\sigma(\operatorname{up}_{\alpha}(\operatorname{rhs}_{\beta}))$, i.e., we obtain \sigma(\operatorname{lhs}_{\alpha\circ\beta})=\sigma(\operatorname{lhs}_{\alpha})\mathrel{\smash{\stackunder[0pt]{\xrightarrow{\makebox[7.50002pt]{$$}}}{\scriptstyle\,}}}^{*}_{\mathcal{T}}\sigma(\operatorname{up}_{\alpha}(\operatorname{rhs}_{\beta}))=\sigma(\operatorname{rhs}_{\alpha\circ\beta}), where the evaluation with $\mathcal{T}$ takes two steps. This proves soundness of Chain. Well-formedness of $\mathcal{T}^{\circ}$ follows from the fact that the valuation $\sigma\circ\operatorname{up}_{\alpha}$ satisfies $\operatorname{guard}_{\beta}$ and $\{\beta\}$ is well formed. ∎

A-C Proof of Thm. 10

Proof.

Well-formedness of $\mathcal{T}^{\omega}$ is trivial. For soundness, let $\sigma$ be a valuation with

[TABLE]

It suffices to prove that $\sigma(\operatorname{lhs}_{\alpha})$ starts a non-terminating run with $\mathcal{T}$. To this end, we prove $\sigma\models\operatorname{up}_{\alpha}^{n}(\operatorname{guard}_{\alpha})$ for all $n\in\mathbb{N}$ by induction on $n$. The induction base is trivial, as $\operatorname{guard}_{\alpha^{\omega}}=\operatorname{guard}_{\alpha}$. For the induction step, let $n>0$. The induction hypothesis implies $\sigma\models\operatorname{up}_{\alpha}^{n-1}(\operatorname{guard}_{\alpha})$. As $\operatorname{guard}_{\alpha}$ is a simple invariant, it implies $\operatorname{up}_{\alpha}(\operatorname{guard}_{\alpha})$ and we obtain $\sigma\models\operatorname{up}_{\alpha}^{n}(\operatorname{guard}_{\alpha})$, which finishes the proof of the theorem. ∎

A-D Proof of Thm. 12

Proof.

Well-formedness of $\mathcal{T}^{\bm{f\!p}}$ is trivial. For soundness, let $\theta$ be a valuation with

[TABLE]

Since $\operatorname{guard}_{\alpha^{\bf{f\!p}}}$ implies $\bm{x}=\operatorname{up}_{\alpha}(\bm{x})$, by induction on $n$ we obtain that

[TABLE]

Hence, $\theta(\operatorname{lhs}_{\alpha})$ starts a non-terminating run, because $\theta\circ\operatorname{up}_{\alpha}^{n}\models\operatorname{guard}_{\alpha}$ for all $n\in\mathbb{N}$. ∎

A-E Proof of Thm. 14

Proof.

The theorem trivially holds, as

[TABLE]

clearly implies

[TABLE]

∎