Abstract We consider the problem of proving termination for triangular weakly non-linear loops (twn-loops) over some ring $$\mathcal {S}$$ S like $$\mathbb {Z}$$ Z , $$\mathbb {Q}$$ Q , or $$\mathbb {R}$$ R . The guard of such a loop is an arbitrary quantifier-free Boolean formula over (possibly non-linear) polynomial inequations, and the body is a single assignment of the form $$\begin{bmatrix} x_1\\ \ldots \\ x_d \end{bmatrix} \leftarrow \begin{bmatrix} c_1 \cdot x_1 + p_1\\ \ldots \\ c_d \cdot x_d + p_d \end{bmatrix}$$ x 1 … x d ← c 1 · x 1 + p 1 … c d · x d + p d where each $$x_i$$ x i is a variable, $$c_i \in \mathcal {S}$$ c i ∈ S , and each $$p_i$$ p i is a (possibly non-linear) polynomial over $$\mathcal {S}$$ S and the variables $$x_{i+1},\ldots ,x_{d}$$ x i + 1 , … , x d . We show that the question of termination can be reduced to the existential fragment of the first-order theory of $$\mathcal {S}$$ S . For loops over $$\mathbb {R}$$ R , our reduction implies decidability of termination. For loops over $$\mathbb {Z}$$ Z and

Abstract We present a novel modular approach to infer upper bounds on the expected runtimes of probabilistic integer programs automatically. To this end, it computes bounds on the runtimes of program parts and on the sizes of their variables in an alternating way. To evaluate its power, we implemented our approach in a new version of our open-source tool .

In the last years, several works were concerned with identifying classes of programs where termination is decidable. We consider triangular weakly non-linear loops (twn-loops) over a ring Z ≤ S ≤ R_A , where R_A is the set of all real algebraic numbers. Essentially, the body of such a loop is a single assignment (x_1, ..., x_d) ← (c_1 · x_1 + pol_1, ..., c_d · x_d + pol_d) where each x_i is a variable, c_i ∈ S, and each pol_i is a (possibly non-linear) polynomial over S and the variables x_{i+1}, ..., x_d. Recently, we showed that termination of such loops is decidable for S = R_A and non-termination is semi-decidable for S = Z and S = Q. In this paper, we show that the halting problem is decidable for twn-loops over any ring Z ≤ S ≤ R_A. In contrast to the termination problem, where termination on all inputs is considered, the halting problem is concerned with termination on a given input. This allows us to compute witnesses for non-termination. Moreover, we present the first computability results on the runtime complexity of such loops. More precisely, we show that for twn-loops over Z one can always compute a polynomial f such that the length of all terminating runs is bounded by f( || (x_1, ..., x_d) || ), where || · || denotes the 1-norm. As a corollary, we obtain that the runtime of a terminating triangular linear loop over Z is at most linear.

We present a new inductive rule for verifying lower bounds on expected values of random variables after execution of probabilistic loops as well as on their expected runtimes. Our rule issimplein the sense that loop body semantics need to be applied only finitely often in order to verify that the candidates are indeed lower bounds. In particular, it is not necessary to find the limit of a sequence as in many previous rules.