Geometric Nontermination Arguments
Abstract
We present a new kind of nontermination argument, called geometric nontermination argument. The geometric nontermination argument is a finite representation of an infinite execution that has the form of a sum of several geometric series. For so-called linear lasso programs we can decide the existence of a geometric nontermination argument using a nonlinear algebraic \(\exists \)-constraint. We show that a deterministic conjunctive loop program with nonnegative eigenvalues is nonterminating if an only if there exists a geometric nontermination argument. Furthermore, we present an evaluation that demonstrates that our method is feasible in practice.
1 Introduction
The problem whether a program is terminating is undecidable in general. One way to approach this problem in practice is to analyze the existence of termination arguments and nontermination arguments. The existence of a certain termination argument like, e.g, a linear ranking function, is decidable [4, 31] and implies termination. However, if we cannot find a linear ranking function we cannot conclude nontermination. Vice versa, the existence of a certain nontermination argument like, e.g, a linear recurrence set [20], is decidable and implies nontermination however, if we cannot find such a recurrence set we cannot conclude termination.
In this paper1 we present a new kind of termination argument which we call geometric nontermination argument (GNTA). Unlike a recurrence set, a geometric nontermination argument does not only imply nontermination, it also explicitly represents an infinite program execution. Hence a user sees immediately if the counterexample to termination is a fixpoint or an unbounded diverging execution. An infinite program execution that is represented by a geometric nontermination argument can be written as a pointwise sum of several geometric series. We show that such an infinite execution exists for each deterministic conjunctive loop program that is nonterminating and whose transition matrix has only nonnegative eigenvalues.
We restrict ourselves to linear lasso programs. A lasso program consists of a single while loop that is preceded by straight-line code. The name refers to the lasso shaped form of the control flow graph. Usually, linear lasso programs do not occur as stand-alone programs. Instead, they are used as a finite representation of an infinite path in a control flow graph. For example, in (potentially spurious) counterexamples in termination analysis [6, 16, 21, 22, 24, 25, 32, 33, 37], stability analysis [11, 34], cost analysis [1, 19], or the verification of temporal properties [7, 13, 14, 15, 18] for programs.
We present a constraint based approach that allow us to check whether a linear conjunctive lasso program has a geometric nontermination argument and to synthesize one if it exists.
Three nonterminating linear lasso programs. Each has an infinite execution which is either a geometric series or a pointwise sum of geometric series. The first lasso program is nondeterministic because the variable b gets some nondeterministic value in each iteration.
In this paper, we formally introduce the notion of a geometric nontermination argument for linear lasso programs (Sect. 3) and we prove that each nonterminating deterministic conjunctive linear loop program whose transition matrix has only nonnegative real eigenvalues has a geometric nontermination argument, i.e., each such nonterminating linear loop program has an infinite execution which can be written as a sum of geometric series (Sect. 4).
2 Preliminaries
We denote vectors \(\varvec{x}\) with bold symbols and matrices with uppercase Latin letters. Vectors are always understood to be column vectors, \(\varvec{1}\) denotes a vector of ones, \(\varvec{0}\) denotes a vector of zeros (of the appropriate dimension), and \(\varvec{e_i}\) denotes the i-th unit vector.
2.1 Linear Lasso Programs
In this work, we consider linear lasso programs, programs that consist of a program step and a single loop. We use binary relations over the program’s states to define the stem and the loop transition relation. Variables are assumed to be real-valued.
We denote by \(\varvec{x}\) the vector of n variables \((x_1, \ldots , x_n)^T \in \mathbb {R}^n\) corresponding to program states, and by \(\varvec{x'} = (x_1', \ldots , x_n')^T \in \mathbb {R}^n\) the variables of the next state.
Definition 1
A linear loop program is a linear lasso program L without stem, i.e., a linear lasso program such that the relation \({\scriptstyle \mathrm {STEM}}\) is equivalent to true.
Definition 2
Definition 3
(Nontermination). A linear lasso program L is nonterminating iff there is an infinite sequence of states \(\varvec{x_0}, \varvec{x_1}, \ldots \), called an infinite execution of L, such that \((\varvec{x_0}, \varvec{x_1}) \in {\scriptstyle \mathrm {STEM}}\) and \((\varvec{x_t}, \varvec{x_{t+1}}) \in {\scriptstyle \mathrm {LOOP}}\) for all \(t \ge 1\).
2.2 Jordan Normal Form
Let \(M \in \mathbb {R}^{n \times n}\) be a real square matrix. If there is an invertible square matrix S and a diagonal matrix D such that \(M = SDS^{-1}\), then M is called diagonalizable. The column vectors of S form the basis over which M has diagonal form. In general, real matrices are not diagonalizable. However, every real square matrix M with real eigenvalues has a representation which is almost diagonal, called Jordan normal form. This is a matrix that is zero except for the eigenvalues on the diagonal and one superdiagonal containing ones and zeros.
Theorem 4
(Jordan Normal Form). For each real square matrix \(M \in \mathbb {R}^{n \times n}\) with real eigenvalues, there is an invertible real square matrix \(V \in \mathbb {R}^{n \times n}\) and a Jordan normal form \(J \in \mathbb {R}^{n \times n}\) such that \(M = V J V^{-1}\).
3 Geometric Nontermination Arguments
Definition 5
- (domain)
-
\(\varvec{x_0}, \varvec{x_1}, \varvec{y_1}, \ldots , \varvec{y_s} \in \mathbb {R}^n\), and \(\lambda _1, \ldots , \lambda _s, \mu _1, \ldots , \mu _{s-1} \ge 0\)
- (initiation)
-
\((\varvec{x_0}, \varvec{x_1}) \in {\scriptstyle \mathrm {STEM}}\)
- (point)
-
\(A \left( {\begin{matrix} {\varvec{x_1}} \\ {\varvec{x_1} + \sum _{k=1}^s \varvec{y_k}} \end{matrix}}\right) \le \varvec{b}\)
- (ray)
-
\(A \left( {\begin{matrix} {\varvec{y_1}} \\ {\lambda _1 \varvec{y_1}} \end{matrix}}\right) \le 0\) and \(A \left( {\begin{matrix} {\varvec{y_i}} \\ {\lambda _i \varvec{y_k} + \mu _{k-1} \varvec{y_{k-1}}} \end{matrix}}\right) \le 0\) for each \(k\in \{2 \ldots s\}\).
The existence of a geometric nontermination argument can be checked using an SMT solver. The constraints given by (domain), (init), (point), (ray) are nonlinear algebraic constraints and the satisfiability of these constraints is decidable.
Proposition 6
(Soundness). If there is a geometric nontermination argument for a linear lasso program L, then L is nonterminating.
Proof
Proposition 7
4 Completeness Results
First we show that a linear loop program has a GNTA if it has is a bounded infinite execution. In the next section we use this to prove our completeness result.
4.1 Bounded Infinite Executions
Let \(|\cdot |: \mathbb {R}^n\rightarrow \mathbb {R}\) denote some norm. We call an infinite execution \((\varvec{x}_t)_{t \ge 0}\) bounded iff there is a real number \(d \in \mathbb {R}\) such that the norm of each state is bounded by d, i.e., \(|\varvec{x}_t|\le d\) for all t (in \(\mathbb {R}^n\) the notion of boundedness is independent of the choice of the norm).
Lemma 8
(Fixed Point). Let \(L = (true, {\scriptstyle \mathrm {LOOP}})\) be a linear loop program. The linear loop program L has a bounded infinite execution if and only if there is a fixed point \(\varvec{x}^*\in \mathbb {R}^n\) such that \((\varvec{x}^*, \varvec{x}^*) \in {\scriptstyle \mathrm {LOOP}}\).
Proof
Note that Lemma 8 does not transfer to lasso programs: there might only be one fixed point and the stem might exclude this point (e.g., \(a = -0.5\) and \(b = 3.5\) in example Fig. 1a).
Because fixed points give rise to trivial geometric nontermination arguments, we can derive a criterion for the existence of geometric nontermination arguments from Lemma 8.
Corollary 9
(Bounded Infinite Executions). If the linear loop program \(L = (true, {\scriptstyle \mathrm {LOOP}})\) has a bounded infinite execution, then it has a geometric nontermination argument of size 0.
Proof
By Lemma 8 there is a fixed point \(\varvec{x}^*\) such that \((\varvec{x}^*, \varvec{x}^*) \in {\scriptstyle \mathrm {LOOP}}\). We choose \(\varvec{x_0} = \varvec{x_1} = \varvec{x}^*\) which satisfies (point) and (ray) and thus is a geometric nontermination argument for L. \(\square \)
Example 10
4.2 Nonnegative Eigenvalues
This section is dedicated to the proof of the following completeness result for deterministic linear loop programs.
Theorem 11
(Completeness). If a deterministic linear loop program L of the form Open image in new window with n variables is nonterminating and M has only nonnegative real eigenvalues, then there is a geometric nontermination argument for L of size at most n.
To prove this completeness theorem, we need to construct a GNTA from a given infinite execution. The following lemma shows that we can restrict our construction to exclude all linear subspaces that have a bounded execution.
Lemma 12
(Loop Disassembly). Let \(L = (true, {\scriptstyle \mathrm {LOOP}})\) be a linear loop program over \(\mathbb {R}^n = \mathcal {U} \oplus \mathcal {V}\) where \(\mathcal {U}\) and \(\mathcal {V}\) are linear subspaces of \(\mathbb {R}^n\). Suppose L is nonterminating and there is an infinite execution that is bounded when projected to the subspace \(\mathcal {U}\). Let \(\varvec{x}^\mathcal {U}\) be the fixed point in \(\mathcal {U}\) that exists according to Lemma 8. Then the linear loop program \(L^{\mathcal {V}}\) that we get by projecting to the subspace \(\mathcal {V} + \varvec{x}^\mathcal {U}\) is nonterminating. Moreover, if \(L^{\mathcal {V}}\) has a GNTA of size s, then L has a GNTA of size s.
Proof
Without loss of generality, we are in the basis of \(\mathcal {U}\) and \(\mathcal {V}\) so that these spaces are nicely separated by the use of different variables. Using the infinite execution of L that is bounded on \(\mathcal {U}\) we can do the construction from the proof of Lemma 8 to get an infinite execution \(\varvec{z_0}, \varvec{z_1}, \ldots \) that yields the fixed point \(\varvec{x}^\mathcal {U}\) when projected to \(\mathcal {U}\). We fix \(\varvec{x}^\mathcal {U}\) in the loop transition by replacing all variables from \(\mathcal {U}\) with the values from \(\varvec{x}^\mathcal {U}\) and get the linear loop program \(L^{\mathcal {V}}\) (this is the projection to \(\mathcal {V} + \varvec{x}^\mathcal {U}\)). Importantly, the projection of \(\varvec{z_0}, \varvec{z_1}, \ldots \) to \(\mathcal {V} + \varvec{x}^{\mathcal {U}}\) is still an infinite execution, hence the loop \(L^{\mathcal {V}}\) is nonterminating. Given a GNTA for \(L^{\mathcal {V}}\) we can construct a GNTA for L by adding the vector \(\varvec{x}^\mathcal {U}\) to \(\varvec{x_0}\) and \(\varvec{x_1}\). \(\square \)
Proof
Let \(P := \{ \varvec{x} \in \mathbb {R}^n \mid G\varvec{x} \le \varvec{g} \}\) denote the guard polyhedron. Its projection \(P^{\overline{\mathcal {Y}}^\bot }\) to the subspace \(\overline{\mathcal {Y}}^\bot \) is again a polyhedron. By the decomposition theorem for polyhedra [36, Corollary 7.1b], \(P^{\overline{\mathcal {Y}}^\bot } = Q + C\) for some polytope Q and some convex cone C. However, by definition of the subspace \(\overline{\mathcal {Y}}^\bot \), the convex cone C must be equal to \(\{ \varvec{0} \}\): for any \(\varvec{y} \in C \subseteq \overline{\mathcal {Y}}^\bot \), we have \(G\varvec{y} \le \varvec{0}\), thus \(\varvec{y} \in \mathcal {Y}\), and therefore \(\varvec{y}\) is orthogonal to itself, i.e., \(\varvec{y} = \varvec{0}\). We conclude that \(P^{\overline{\mathcal {Y}}^\bot }\) must be a polytope, and thus it is bounded. By assumption L is nonterminating, so \(L^{\overline{\mathcal {Y}}^\bot }\) is nonterminating, and since \(P^{\overline{\mathcal {Y}}^\bot }\) is bounded, any infinite execution of \(L^{\overline{\mathcal {Y}}^\bot }\) must be bounded.
Let \(\mathcal {U}\) denote the direct sum of the generalized eigenspaces for the eigenvalues \(0 \le \lambda < 1\). Any infinite execution is necessarily bounded on the subspace \(\mathcal {U}\) since on this space the map \(\varvec{x} \mapsto M\varvec{x} + \varvec{m}\) is a contraction. Let \(\mathcal {U}^\bot \) denote the subspace of \(\mathbb {R}^n\) orthogonal to \(\mathcal {U}\). The space \(\overline{\mathcal {Y}} \cap \mathcal {U}^\bot \) is a linear subspace of \(\mathbb {R}^n\) and any infinite execution in its complement is bounded. Hence we can turn our analysis to the subspace \(\overline{\mathcal {Y}} \cap \mathcal {U}^\bot + \varvec{x}\) for some \(\varvec{x} \in \overline{\mathcal {Y}}^\bot \oplus \mathcal {U}\) for the rest of the proof according to Lemma 12. From now on, we implicitly assume that we are in this space without changing any of the notation.
Part 1. In this part we show that there is a basis \(\varvec{y_1}, \ldots , \varvec{y_s} \in \mathcal {Y}\) such that M turns into a matrix U of the form given in (1) with \(\lambda _1, \ldots , \lambda _s, \mu _1, \ldots , \mu _{s-1} \ge 0\). Since we allow \(\mu _k\) to be positive between different eigenvalues (Example 14 illustrates why), this is not necessarily a Jordan normal form and the vectors \(\varvec{y_i}\) are not necessarily generalized eigenvectors.
We choose a basis \(\varvec{v_1}, \ldots , \varvec{v_s}\) such that M is in Jordan normal form with the eigenvalues ordered by size such that the largest eigenvalues come first. Define \(\mathcal {V}_1 := \overline{\mathcal {Y}} \cap \mathcal {U}^\bot \) and let \(\mathcal {V}_1 \supset \ldots \supset \mathcal {V}_s\) be a strictly descending chain of linear subspaces where \(\mathcal {V}_i\) is spanned by \(\varvec{v_k}, \ldots , \varvec{v_s}\).
We distinguish two cases. First, if \(\lambda _{k-1} \ne \lambda _k\), then \(\lambda _j - \lambda _k\) is positive for all \(j < k\) because larger eigenvalues come first. Since N is nilpotent and upper triangular, \(N \sum _{j \le k} \alpha _{k,j} \varvec{e_j}\) is a linear combination of \(\varvec{e_1}, \ldots , \varvec{e_{k-1}}\) (i.e., only the first \(k-1\) entries are nonzero). Whatever values this vector assumes, we can increase the parameters \(\alpha _{k,j}\) for \(j < k\) to make (11) larger and increase the parameters \(\alpha _{k-1,j}\) for \(j < k\) to make (11) smaller.
Importantly, there are no cyclic dependencies in the values of \(\alpha \) because neither one of the coefficients \(\alpha \) can be made too large. Therefore we can choose \(\alpha \ge 0\) such that (10) is satisfied for all \(k > 1\) and hence the basis \(\varvec{y_1}, \ldots , \varvec{y_s}\) brings M into the desired form (1).
Part 2. In this part we construct the geometric nontermination argument and check the constraints from Definition 5. Since L has an infinite execution, there is a point \(\varvec{x}\) that fulfills the guard, i.e., \(G\varvec{x} \le \varvec{g}\). We choose \(\varvec{x_1} := \varvec{x} + Y\varvec{\gamma }\) with \(\varvec{\gamma }\ge \varvec{0}\) to be determined later. Moreover, we choose \(\lambda _1, \ldots , \lambda _s\) and \(\mu _1, \ldots , \mu _{s-1}\) from the entries of U given in (1). The size of our GNTA is s, the number of vectors \(\varvec{y_1}, \ldots , \varvec{y_s}\). These vectors form a basis of \(\overline{\mathcal {Y}} \cap \mathcal {U}^\bot \), which is a subspace of \(\mathbb {R}^n\); thus \(s \le n\), as required.
We proceed for each (not quite Jordan) block of U separately, i.e., we assume that we are looking at the subspace \(\varvec{y_j}, \ldots , \varvec{y_k}\) with \(\mu _k = \mu _{j-1} = 0\) and \(\mu _\ell > 0\) for all \(\ell \in \{j,\ldots ,k-1\}\). If this space only contains eigenvalues that are larger than 1, then \(U - I\) is invertible and has only nonnegative entries. By using large enough values for \(\varvec{\beta }\), we can make \(\varvec{\tilde{x}}\) and \(\varvec{\tilde{m}}\) small enough, such that \(\varvec{1} \ge (U - I)\varvec{\tilde{x}} + \varvec{\tilde{m}}\). Then we just need to pick \(\varvec{\gamma }\) appropriately.
If there is at least one eigenvalue 1, then \(U - I\) is not invertible, so (13) could be overconstraint. Notice that \(\mu _\ell > 0\) for all \(\ell \in \{j,\ldots ,k-1\}\), so only the bottom entry in the vector Eq. (13) is not covered by \(\varvec{\gamma }\). Moreover, since eigenvalues are ordered in decreasing order and all eigenvalues in our current subspace are \(\ge 1\), we conclude that the eigenvalue for the bottom entry is 1. (Furthermore, k is the highest index since each eigenvalue occurs only in one block). Thus we get the equation \(\varvec{\tilde{m}}_k = 1\). If \(\varvec{\tilde{m}}_k\) is positive, this equation has a solution since we can adjust \(\varvec{\beta }_k\) accordingly. If it is zero, then the execution on the space spanned by \(\varvec{y_k}\) is bounded, which we can rule out by Lemma 12.
It remains to rule out that \(\varvec{\tilde{m}}_k\) is negative. Let \(\mathcal {U}\) be the generalized eigenspace to the eigenvector 1 and use Lemma 13 below to conclude that \(\varvec{o} := N^{s-1}\varvec{m} + \varvec{u} \in \mathcal {Y}\) for some \(\varvec{u} \in \mathcal {U}^\bot \). We have that \(M\varvec{o} = M(N^{s-1}\varvec{m} + \varvec{u}) = M\varvec{u} \in \mathcal {U}^\bot \), so \(\varvec{o}\) is a candidate to pick for the vector \(\varvec{w_k}\). Therefore without loss of generality we did so in part 1 of this proof and since \(\varvec{y_k}\) is in the convex cone spanned by the basis \(\varvec{w_1}, \ldots , \varvec{w_s}\) we get \(\varvec{\tilde{m}}_k > 0\). \(\square \)
Lemma 13
(Deterministic Loops with Eigenvalue 1). Let \(M = I + N\) and let N be nilpotent with nilpotence index k (\(k := \min \{ i \mid N^i = 0 \}\)). If \(GN^{k-1} \varvec{m} \not \le \varvec{0}\), then L is terminating.
Proof
We show termination by providing an k-nested ranking function [28, Definition 4.7]. By [28, Lemma 3.3] and [28, Theorem 4.10], this implies that L is terminating.
Example 14
5 Experiments
We implemented our method in a tool that is specialized for the analysis of lasso programs and called Ultimate LassoRanker2. LassoRanker is used by Ultimate Büchi Automizer [22] which analyzes termination of (general) C programs. Büchi Automizer iteratively picks lasso shaped paths in the control flow graph converts them to lasso programs and lets LassoRanker analyze them. In case LassoRanker was able to prove nontermination a real counterexample to termination was found, in case LassoRanker was able to provide a termination argument (e.g., a linear ranking function), Büchi Automizer continues the analysis, but only on lasso shaped paths for which the termination arguments obtained in former iterations are not applicable.
We applied Büchi Automizer to the 803 C programs from the Termination Competition 20173 Our constraints for the existence of a geometric nontermination arguments (GNTA) were stated over the integers and we used the SMT solver Z3 [23] with a timeout of 12 s to solve these constraints. The overall timeout for the termination analysis was 60s. In our implementation, LassoRanker first tries to find a fixpoint for a lasso and only if not fixpoint exists, it tries to find a GNTA that can also represent an unbounded execution. The tool was able to identify 143 nonterminating programs. For 82 of these a fixpoint was detected. For the other 61 programs the counterexample had only an unbounded execution but not fixpoint.
This experiment demonstrates that despite the nonlinear integer constraint the synthesis of GNTA is feasible in practice and that furthermore GNTAs which can also represent unbounded executions improved Büchi Automizer significantly.
6 Related Work
One line of related work is focused on decidability questions for deterministic lasso programs. Tiwari [38] considered linear loop programs over the reals where only strict inequalities are used in the guard and proved that termination is decidable. Braverman [5] generalized this result to loop programs that use strict and non-strict inequalities in the guard. Furthermore, he proved that termination is also decidable for homogeneous deterministic loop programs over the integers. Rebiha et al. [35] generalized the result to integer loops where the update matrix has only real eigenvalues. Ouaknine et al. [30] generalized the result to integer lassos where the update matrix of the loop is diagonalizable.
Another line of related work is also applicable to nondeterministic programs and uses a constraint-based synthesis of recurrence sets. The recurrence sets are defined by templates [20, 39] or the constraint is given in a second order theory for bit vectors [17]. These approaches can be used to find nonterminating lassos that do not have a geometric nontermination argument; however, this comes at the price that for nondeterministic programs an \(\exists \forall \exists \)-constraint has to be solved.
Furthermore, there is a long line of research [2, 3, 8, 9, 10, 12, 17, 26, 27] that addresses programs that are more general than lasso programs.
7 Conclusion
We presented a new approach to nontermination analysis for (nondeterministic) linear lasso programs. This approach is based on geometric nontermination arguments, which are an explicit representation of an infinite execution. Unlike, e.g., a recurrence set which encodes a set of nonterminating executions, a user can immediate see if our nonterminating proof encodes a fixpoint or a diverging unbounded execution. Our nontermination arguments can be found by solving a set of nonlinear constraints. In Sect. 4 we showed that the class of nonterminating linear lasso programs that have a geometric nontermination argument is quite large: it contains at least every deterministic linear loop program whose eigenvalues are nonnegative. We expect that this statement can be extended to encompass also negative and complex eigenvalues.
Footnotes
References
- 1.Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-form upper bounds in static cost analysis. J. Autom. Reasoning 46(2), 161–203 (2011)MathSciNetCrossRefGoogle Scholar
- 2.Atig, M.F., Bouajjani, A., Emmi, M., Lal, A.: Detecting fair non-termination in multithreaded programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 210–226. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_19CrossRefGoogle Scholar
- 3.Bakhirkin, A., Piterman, N.: Finding recurrent sets with backward analysis and trace partitioning. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 17–35. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_2CrossRefGoogle Scholar
- 4.Ben-Amram, A.M., Genaim, S.: Ranking functions for linear-constraint loops. In: POPL (2013)Google Scholar
- 5.Braverman, M.: Termination of integer linear programs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 372–385. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_34CrossRefGoogle Scholar
- 6.Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 413–429. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_28CrossRefGoogle Scholar
- 7.Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 387–393. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_22CrossRefGoogle Scholar
- 8.Brockschmidt, M., Ströder, T., Otto, C., Giesl, J.: Automated detection of non-termination and nullpointerexceptions for Java Bytecode. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 123–141. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31762-0_9CrossRefGoogle Scholar
- 9.Urban, C., Gurfinkel, A., Kahsai, T.: Synthesizing ranking functions from bits and pieces. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 54–70. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_4CrossRefGoogle Scholar
- 10.Chen, H.-Y., Cook, B., Fuhs, C., Nimkar, K., O’Hearn, P.: Proving nontermination via safety. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 156–171. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_11CrossRefGoogle Scholar
- 11.Cook, B., Fisher, J., Krepska, E., Piterman, N.: Proving stabilization of biological systems. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 134–149. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_11CrossRefGoogle Scholar
- 12.Cook, B., Fuhs, C., Nimkar, K., O’Hearn, P.W.: Disproving termination with overapproximation. In: FMCAD 2014, pp. 67–74. IEEE (2014)Google Scholar
- 13.Cook, B., Khlaaf, H., Piterman, N.: On automation of CTL* verification for infinite-state systems. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015, Part I. LNCS, vol. 9206, pp. 13–29. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_2CrossRefMATHGoogle Scholar
- 14.Cook, B., Khlaaf, H., Piterman, N.: Verifying increasingly expressive temporal logics for infinite-state systems. J. ACM 64(2), 15:1–15:39 (2017)MathSciNetCrossRefGoogle Scholar
- 15.Cook, B., Koskinen, E., Vardi, M.: Temporal property verification as a program analysis task. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 333–348. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_26CrossRefGoogle Scholar
- 16.Cook, B., Podelski, A., Rybalchenko, A.: Terminator: beyond safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 415–418. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_37CrossRefGoogle Scholar
- 17.David, C., Kroening, D., Lewis, M.: Unrestricted termination and non-termination arguments for bit-vector programs. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 183–204. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46669-8_8CrossRefMATHGoogle Scholar
- 18.Dietsch, D., Heizmann, M., Langenfeld, V., Podelski, A.: Fairness modulo theory: a new approach to LTL software model checking. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015, Part I. LNCS, vol. 9206, pp. 49–66. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_4CrossRefGoogle Scholar
- 19.Gulwani, S., Zuleger, F.: The reachability-bound problem. In: PLDI, pp. 292–304 (2010)Google Scholar
- 20.Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.-G.: Proving non-termination. In: POPL, pp. 147–158 (2008)CrossRefGoogle Scholar
- 21.Harris, W.R., Lal, A., Nori, A.V., Rajamani, S.K.: Alternation for termination. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 304–319. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15769-1_19CrossRefGoogle Scholar
- 22.Heizmann, M., Hoenicke, J., Podelski, A.: Termination analysis by learning terminating programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 797–813. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_53CrossRefGoogle Scholar
- 23.Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339–354. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_27CrossRefGoogle Scholar
- 24.Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop summarization using abstract transformers. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 111–125. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-88387-6_10CrossRefGoogle Scholar
- 25.Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.M.: Termination analysis with compositional transition invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 89–103. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_9CrossRefGoogle Scholar
- 26.Larraz, D., Nimkar, K., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Proving non-termination using max-SMT. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 779–796. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_52CrossRefGoogle Scholar
- 27.Le, T.C., Qin, S., Chin, W.: Termination and non-termination specification inference. In: PLDI, pp. 489–498. ACM (2015)CrossRefGoogle Scholar
- 28.Leike, J., Heizmann, M.: Ranking templates for linear loops. Log. Methods Comput. Sci. 11(1), 1–27 (2015)MathSciNetCrossRefGoogle Scholar
- 29.Leike, J.M., Heizmann, M.: Geometric nontermination arguments. CoRR, abs/1609.05207 (2016)Google Scholar
- 30.Ouaknine, J., Pinto, J.S., Worrell, J.: On termination of integer linear loops. In: Symposium on Discrete Algorithms, pp. 957–969 (2015)Google Scholar
- 31.Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24622-0_20CrossRefGoogle Scholar
- 32.Podelski, A., Rybalchenko, A.: Transition invariants. In LICS, pp. 32–41 (2004)Google Scholar
- 33.Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: POPL, pp. 132–144 (2005)CrossRefGoogle Scholar
- 34.Podelski, A., Wagner, S.: A sound and complete proof rule for region stability of hybrid systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 750–753. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71493-4_76CrossRefGoogle Scholar
- 35.Rebiha, R., Matringe, N., Moura, A.V.: Characterization of termination for linear homogeneous programs. Technical report, Institute of Computing, University of Campinas, March 2014Google Scholar
- 36.Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Hoboken (1999)MATHGoogle Scholar
- 37.Ströder, T., Giesl, J., Brockschmidt, M., Frohn, F., Fuhs, C., Hensel, J., Schneider-Kamp, P., Aschermann, C.: Automatically proving termination and memory safety for programs with pointer arithmetic. J. Autom. Reason. 58(1), 33–65 (2017)MathSciNetCrossRefGoogle Scholar
- 38.Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 70–82. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27813-9_6CrossRefGoogle Scholar
- 39.Velroyen, H., Rümmer, P.: Non-termination checking for imperative programs. In: Beckert, B., Hähnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 154–170. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-79124-9_11CrossRefGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.