Proving termination through conditional termination

Proving Termination through Conditional Termination? Cristina Borralleras1, Marc Brockschmidt2, Daniel Larraz3, Albert Oliveras3, Enric Rodr´ıguez-Carbonell3, and Albert Rubio3 1Universitat de Vic - Universitat Central de Catalunya 2Microsoft Research, Cambridge 3Universitat Polit`ecnica de Catalunya Abstract. We present a constraint-based method for proving conditional termination of integer programs. Building on this, we construct a framework to prove (unconditional) program termination using a powerful mechanism to combine conditional termination proofs. Our key insight is that a conditional termination proof shows termination for a subset of program execution states which do not need to be considered in the remaining analysis. This facilitates more effective termination as well as non-termination analyses, and allows handling loops with different execution phases naturally. Moreover, our method can deal with sequences of loops compositionally. In an empirical evaluation, we show that our implementation VeryMax outperforms state-of-the-art tools on a range of standard benchmarks. 1 Introduction Proving program termination requires not only synthesizing termination arguments, but also reasoning about reachability of program states, as most non-trivial programs contain subprocedures or loops that only terminate for the executions that actually reach them. Thus, a termination prover has to segment the program state space according to its termination behavior, ignoring non-terminating but unreachable states. Recent advances in termination proving try to tackle this problem by abducing conditions for non-termination, and focusing the termination proof search on the remaining state space [25,32]. However, these techniques rely on relatively weak non-termination proving techniques. Furthermore, different termination arguments may be required depending on how a loop or subprocedure is reached, and thus, even though no non-termination argument can be found, the state space needs to be segmented. In this work, we propose to use preconditions for termination to drive the unconditional termination proof. The key insight is that a condition φ implying ? This work was partially supported by the project TIN2015-69175-C4-3-R (MINECO/ FEDER) and by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement ERC-2014-CoG 648276 AUTAR). Borralleras, C. [et al.]. Proving termination through conditional termination. A: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. "Tools and Algorithms for the Construction and Analysis of Systems, 23rd International Conference, TACAS 2017: held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017: Uppsala, Sweden, April 22-29, 2017: proceedings, part I". Berlín: Springer, 2017, p. 99-117. The final authenticated version is available online at https://doi.org/10.1007/978-3-662-54577-5_6 2 C. Borralleras et al. termination allows a termination prover to focus on those program states in which ¬φ holds. To obtain preconditions for termination, we introduce a new constraint-based method that analyzes program components (i.e., loops or subprocedures) independently and synthesizes termination arguments together with a conditional supporting invariant [12]. To prove full program termination, we use a novel program transformation we call unfolding which syntactically splits terminating from potentially non-terminating states using the generated termination conditions. This allows us to combine several conditional termination arguments, each obtained for a small component of the program independently, into a proof for the input program. In summary, we present the following contributions: – A new method based on Max-SMT for finding preconditions for termination (cf. Sect. 3 and Algo. 1). – A framework to prove termination or non-termination by repeatedly simplifying the program analysis task by combining conditional termination arguments using the unfolding transformation (cf. Sect. 4 and Algo. 2). – An implementation of the technique in our tool VeryMax for C++ input programs and an extensive experimental evaluation showing that it is not only more powerful than existing tools, but also more efficient (cf. Sect. 5). 2 Preliminaries SAT, Max-SAT, and Max-SMT. Let P be a fixed set of propositional variables. For p∈ P , p and ¬p are literals. A clause is a disjunction of literals l1∨· · ·∨ln . A (CNF) propositional formula is a conjunction of clauses C1∧ · · · ∧ Cm . The problem of propositional satisfiability (SAT) is to determine whether a propositional formula F has a model, i.e., an assignment M that satisfies F , denoted by M| = F . An extension of SAT is Satisfiability Modulo Theories (SMT) [6], where one checks the satisfiability of a formula with literals from a given background theory. Another extension is (weighted partial) Max-SAT [6], where some clauses in the input formula are soft clauses with an assigned weight, and the others are hard clauses. Here, we look for a model of the hard clauses that maximizes the sum of the weights of the satisfied soft clauses. Finally, Max-SMT combines Max-SAT and SMT. In a Max-SMT problem a formula is of the form H1∧. . .∧Hn∧ [ S1, ω1 ] ∧. . .∧ [ Sm, ωm ], where the hard clauses Hi and the soft clauses Sj (with weight ωj ) are disjunctions of literals over a background theory, and the aim is to find a model of the hard clauses that maximizes the sum of the weights of the satisfied soft clauses. Programs and States. We fix a set of integer program variables V = {v1, . . . , vn} and denote by F(V) the conjunctions of linear inequalities over the variables V. Let L be the set of program locations, which contains a canonical initial location `init . Program transitions are tuples ( `s, ρ, `t ), where `s and `t∈ L are the source and target locations respectively, and ρ∈F ( V ∪ V0 ) describes the transition relation. Here V0 = {v0 1, . . . , v0 n} represent the values of the program variables after the transition.4 4For ϕ∈F(V), we denote by ϕ0∈F(V0) the version of ϕusing primed variables. Proving Termination through Conditional Termination 3 Aprogram P is a set of transitions. 5 The set of locations in these transitions is denoted by L ( P ). We identify a program with its control-flow graph (CFG), a directed graph in which nodes are the locations and edges are the transitions. 6 Aprogram component C of a program P is the set of transitions of a strongly connected component (SCC) of the CFG of P . Its entry transitions EC are those transitions τ = ( `s, ρ, `t ) such that τ6∈ C but `t∈ L ( C ) (and in this case `t is called an entry location), while its exit transitions XC are such that τ6∈ C but `s∈ L(C) (and then `sis an exit location). Astate s = ( `, v ) consists of a location `∈ L and a valuation v : V → Z .Initial states are of the form ( `init, v ). We denote a computation step with transition τ = ( `s, ρ, `t ) by ( `s, v ) →τ ( `t, w ), where ( v , w ) | = ρ . We use →P if we do not care about the executed transition of P , and →∗ P to denote the transitive-reflexive closure of →P. Sequences of computation steps are called computations. Safety and Termination. An assertion ( `, ϕ ) is a pair of a location ` and a formula ϕ∈F ( V ). A program P is safe for the assertion ( `, ϕ ) if for every computation starting at an initial state s0 of the form s0→∗ P ( `, v ), we have that v| = ϕ holds. Safety can be proved using conditional invariants [12], which like ordinary invariants are inductive, but not necessarily initiated in all computations. Definition 1 (Conditional Inductive Invariant). Let P be a program. We say a map Q : L ( P ) →F ( V )is a conditional (inductive) invariant for P if for all (`s, v)→P(`t, w), we have v|=Q(`s)implies w|=Q(`t). A program P is terminating if any computation starting at an initial state is finite. An important tool for proving termination are ranking functions: Definition 2 (Ranking Function). Let C be a component of a program P , and τ= (`s, ρ, `t)∈ C. A function R:Zn→Zis a ranking function for τif: –ρ|=R ≥ 0[Boundedness] –ρ|=R>R0[Decrease] and for every (ˆ `s,ˆρ, ˆ `t)∈ C, –ˆρ|=R≥R0[Non-increase] The key property of ranking functions is that if a transition admits one, then it cannot be executed infinitely. A core concept in our approach is conditional termination, i.e., the notion that once a condition holds, a program is definitely terminating. As we make heavy use of the program’s control flow graph structure, we introduce this concept as location-dependent. 5 Hence in our programming model procedure calls are not allowed. Note however that programs with non-recursive calls can also be handled by inlining the calls. 6 Since we label transitions only with conjunctions of linear inequalities, disjunctive conditions are represented using several transitions with the same source and target location. Thus, Pis actually a multigraph. 4 C. Borralleras et al. int x,y,z; x=nondet(); y=nondet(); z=nondet(); while (y≥0 && z6= 0) { if (z≥0) { x=x−z; y=y+x; z=z+ 1; }else { y=y+z; z=z−1; } } `0`1`2 τ0:true τ1:y≥0∧z > 0 ∧x0=x−z ∧y0=y+x ∧z0=z+ 1 τ2:y≥0∧z < 0 ∧x0=x ∧y0=y+z ∧z0=z−1 τ3:y < 0∧x0=x ∧y0=y∧z0=z τ4:z= 0 ∧x0=x ∧y0=y∧z0=z Fig. 1. Program and its CFG. Definition 3 (Conditional Termination). We say that a program P is ( `, ϕ )- conditionally terminating if every computation that contains a state ( `, v )with v| = ϕ uses transitions from P only a finite number of times. In that case the assertion (`, ϕ)is called a precondition for termination. 3 Synthesizing Conditional Termination Arguments Our approach for synthesizing conditional termination arguments works on one program component at a time. As proving that a program terminates is equivalent to showing that there is no program component where a computation can stay indefinitely, this turns out to be a convenient way to decompose termination proofs. For a fixed program component C , a conditional lexicographic termination argument is constructed iteratively by transition elimination as follows. In each iteration, we synthesize a linear ranking function together with supporting conditional invariants, requiring that they show that at least one transition of C is finitely executable, i.e., can only occur a finite number of times in any execution. The intuition here is that once we have proven that a transition τ can only be used finitely often, we only need to consider (possibly infinite) suffixes of program executions in which τ cannot appear anymore. If after some iterations no transition of C can be executed infinitely anymore, then the conjunction of all conditional invariants obtained at an entry location of C yields a precondition for termination. Indeed, once the conditional invariants hold at that entry location, then by inductiveness they hold from then on at all locations of C , and hence the termination argument applies. Example 1. Consider the program in Fig. 1 and its CFG, with initial location `init = `0 . We want to find a precondition for termination of the component C={τ1, τ2}, corresponding to the while loop. Proving Termination through Conditional Termination 5 For τ= (`s, ρ, `t): Initiation: Iτ def =ρ⇒I0 `t Consecution: Cτ def =I`s∧ρ⇒I0 `t Boundedness: Bτ def =I`s∧ρ⇒R≥0 Decrease: Dτ def =I`s∧ρ⇒R > R0 Non-increase: Nτ def =I`s∧ρ⇒R≥R0 Fig. 2. Constraints used for generating preconditions for termination. In a first iteration, we generate the ranking function y for τ2 , together with the supporting conditional invariant z < 0. Note that z < 0 is indeed a conditional invariant: it is preserved by τ2 as z decreases its value, and is also trivially preserved by τ1 since this transition is in fact disabled if z < 0. Under the condition z < 0, y is bounded and decreases in τ2 , and τ1 is disabled and so finitely executable. Hence, (`1, z < 0) is a precondition for termination.  As observed in [9, 30], synthesizing lexicographic termination arguments together with supporting invariants requires to keep several copies of the program under analysis. Thus, in the analysis of a component C , we keep a set M of possibly infinitely executable transitions (i.e., those for which we have not proved conditional termination yet), called the ter m ination component. Nonetheless, to compute sound invariants (i.e., soundly reason about reachable states), we need to take all transitions into account. However, these transitions can be strengthened with the supporting invariants that we synthesized in earlier proof steps. Hence, we keep another copy I , called the conditional i nvariant component, which is like the original component C , except for the addition of the conditional invariants found in previous iterations. Initially both the termination and the conditional invariant components are identical copies of the component C. The proposed method for generating preconditions for termination is an extension of the constraint-based approach for proving (unconditional) termination presented in [30]. The individual constraints used in our method are displayed in Fig. 2, corresponding to the standard constraints employed in constraint-based techniques [8]. For all locations ` in C , we introduce templates I` corresponding to fixed-length conjunctions of linear inequalities on the program variables; i.e., I` is of the form V1≤i≤k ( ai + Pv∈V ai,vv≤ 0) for some k and where the a∗ are integer template variables that do not appear in V . Furthermore, we also define a template R for a linear ranking function 7 with integer coefficients, i.e., R is of the form a + Pv∈V avv . For a given component C with entries EC , we combine 7 While using a different ranking function for each program location is possible, we have found that the added power does not justify the increased complexity of the ensuing SMT problem. 6 C. Borralleras et al. these constraints in the (non-linear) formula Fas follows: Fdef =^ τ∈EC Iτ∧^ τ∈I Cτ∧^ τ∈M Nτ∧_ τ∈M (Bτ∧Dτ). However, not all of these constraints are treated as hard constraints. Most notably, we turn Vτ∈EC Iτ into soft constraints. Intuitively this means that, if possible, we want to synthesize a true (unconditional) supporting invariant, but will also allow invariants that do not always hold. However, we keep Vτ∈I Cτ as a hard constraint, ensuring that our conditional invariants are indeed inductive, i.e., keep on holding after they have been satisfied once. Similarly, Vτ∈M Nτ∧Wτ∈M ( Bτ∧Dτ ) are kept as hard constraints, enforcing that a true ranking function is found, though it may only hold in those cases where the supporting invariant is initiated. The conditions for the supporting invariants will eventually become our preconditions for termination. Algo. 1 shows our procedure CondTerm for generating preconditions for termination. It takes as inputs the component Cunder consideration and its entry transitions EC , and returns a conditional invariant Q that ensures that no infinite computation can remain within C. Algorithm 1 Procedure CondTerm for computing preconditions for termination Input: component C, entry transitions EC Output: None | Q, where Qmaps locations in L(C) to conjunctions of inequalities 1: (I,M)←(C,C) 2: Q ← { `7→ true |`∈ L(C)} 3: while M 6=∅do 4: construct formula Ffrom I,M,EC 5: σ←Max-SMT-solver(F) 6: if σis a solution then 7: I ← { (`s, ρ ∧σ(I`s), `t)|(`s, ρ, `t)∈ I } 8: M ← { (`s, ρ ∧σ(I`s), `t)|(`s, ρ, `t)∈ M } 9: M ← M − { τ∈ M | σ(R) is a ranking function for τ} 10: Q ← { `7→ Q(`)∧σ(I`)|`∈ L(C)} 11: else return None 12: return Q In Algo. 1, we continue to extend the termination argument as long as there are still potentially infinitely executable transitions (line 3). For this, we build a MaxSMT problem F to generate a ranking function and its supporting conditional invariants. If no solution can be found, then the procedure gives up (line 11). Otherwise, a solution σ to F yields a linear function σ ( R ) (the instantiation of the template ranking function R determined by σ ) together with conditional invariants σ ( I`s ). Since the σ ( I`s ) are conditional invariants, they can be used to strengthen transitions τ = ( `s, ρ, `t ) by conjoining σ ( I`s ) to ρ , both in the conditional invariant component and in the termination component (lines 7-8). Proving Termination through Conditional Termination 7 Most importantly, we identify the subset of the transitions τ from M for which σ ( R ) is a ranking function, and hence can be removed from M (line 9). Finally, conditional invariants from previous iterations are accumulated so that, in the end, a global conjunction can be returned (lines 10 and 12). In essence, this process corresponds to the step-wise construction of a lexicographic termination argument. For a location ` at which the component C is entered, the conjunction of all obtained σ ( I` ) is then a precondition for termination. The following theorem states the correctness of procedure CondTerm : Theorem 1 (CondTerm soundness). Let P be a program, C a component, and EC its entry transitions. If the procedure call CondTerm ( C,EC )returns Q 6 = None , then Cis (`, Q(`))-conditionally terminating for any `∈ L(C). Of course, Algo. 1 is an idealized, high-level description of our procedure. In an implementation of the procedure CondTerm , a number of small changes help to improve the overall number of solved instances. Constraint Strengthening. Additional constraints can be added to formula F to favor conditional invariants that are more likely to be useful. In particular, a constraint requiring that the conditional invariants are compatible with the entry transitions and with the previously generated conditional invariants has proven useful, i.e. _ (`s, ρ, `t)∈EC ∃V,V0(I0 `t∧ρ∧ Q(`t)0). Constraint Softening. Similarly, we can increase the allowed range of models by turning more of the clauses into soft clauses. For example, this can be used to allow quasi-ranking functions [30] in addition to ranking functions. Quasi-ranking functions are functions that satisfy the non-increase condition, but may fail to decrease or be bounded, or both. By using them to partition transitions and perform case analysis, programs can also be shown to be terminating. Pseudo-Invariants of Termination Component. In some circumstances, inductive properties of the termination component M(i.e., satisfying Consecution only for transitions in M ) can be sound and useful; namely, when the complement of the property disables a transition. Formally, let Q be a map from L ( P ) to F ( V ) such that Q ( ˜ `s ) ∧˜ρ⇒ Q ( ˜ `t ) 0 for all ( ˜ `s,˜ρ, ˜ `t ) ∈ M , and ¬ Q ( `s ) ∧ρ| = false for some τ = ( `s, ρ, `t ) ∈ M . Moreover, assume that Q supports a ranking function R for τ . Then τ can only be used finitely often. To see this, assume that there is an infinite computation in which τ occurs infinitely often. Then there is a state at location `s in the computation from which only transitions in M are taken. Since Q is inductive over transitions in M , if Q ( `s ) holds at that state then it holds from then on, and therefore R proves that τ cannot be executed an infinite number of times. Otherwise, if Q ( `s ) does not hold, then τ cannot be executed at all. This weaker requirement on Q allows removing transitions from M and is easier to satisfy. Still, it is insufficient to do a case analysis as a full conditional invariant allows. 8 C. Borralleras et al. `0 `1 b `1 `2 τ0:true τ1:y≥0∧z > 0 ∧x0=x−z ∧y0=y+x ∧z0=z+ 1 τ2:y≥0∧z < 0 ∧x0=x ∧y0=y+z ∧z0=z−1 τ3:y < 0 ∧x0=x ∧y0=y ∧z0=z τ4:z= 0 ∧x0=x ∧y0=y ∧z0=z τ0∧z0≥0 τ1∧z0≥0τ2∧z0≥0 τ3 τ4 τ0∧z0<0 τ1∧z < 0τ2∧z < 0 τ2∧z0<0 τ1∧z0<0 τ3 τ4 `0`1`2 τ0∧z0≥0 τ1∧z0≥0 τ3 τ4 `0`1`2 τ0∧z0≥0 ∧x0≥0 τ1∧z0≥0∧x0≥0 τ3 τ4 (a) (b) (c) Fig. 3. Unfolding of the program from Fig. 1 for conditional invariant z < 0 at `1(a), ensuing narrowing/simplification ( b ) and narrowing after unfolding for x < 0 at `1 ( c ). 4 Proving Termination using Conditional Termination Our key contribution is to leverage conditional termination arguments to perform a natural case analysis of program executions. In this way, as our analysis progresses, more and more program runs are excluded from the program analysis, allowing the method to focus on those parts of the program for which termination has not been guaranteed yet. The core component of this is a syntactic program transformation we call unfolding that implements the semantic intuition of distinguishing program states for which termination has not been proven yet. 4.1 Program Unfoldings We begin this subsection with an example that illustrates how conditional invariants can be used to unfold the component under consideration. Example 2. Consider the program from Fig. 1 again. In Ex. 1 it was shown that all computations for which z < 0 holds at location `1 are finite. In fact, a byproduct of the proof was that z < 0 is a conditional invariant at location `1 . We show how to exploit this to prove unconditional termination next. Following the intuition of a case analysis, we unfold the program component by introducing a copy of it in which we assume that the conditional invariant Proving Termination through Conditional Termination 9 holds. In our example, we duplicate the location `1 , introducing a copy denoted by b `1 . We also duplicate all transitions in, from and to the component, using the newly introduced location. However, all copied transitions should also reflect our case analysis, and are thus strengthened by the conditional invariant z < 0. In our case analysis, the original component now corresponds to the case that the conditional invariant does not hold, and thus, all of the original transitions are strengthened to assume the negation of the conditional invariant. Finally, to allow for computations where the invariant eventually becomes true, we add copies of the transitions from the original component to the copied location, again strengthened by the invariant. The resulting program is shown in Fig. 3(a). The original program and its unfolding behave equivalently, in particular regarding termination. However, we already know from Ex. 1 that under the assumption z < 0, the new component has no infinite executions. Hence, we can narrow the set of potentially infinite computations and focus on the program shown in Fig. 3(b), obtained by removing all known-terminating locations (i.e., b `1 ) from the unfolding and simplifying. If this narrowed program terminates, we can conclude that the original program terminates too. Synthesizing another conditional termination argument for the program from Fig. 3(b) now yields the ranking function y , supported by the conditional invariant x < 0 at `1 . Then we can unfold with x < 0 again and narrow, obtaining the program in Fig. 3(c). Finally this program can be proven terminating with ranking function x without the need of any conditional invariant and, hence, without precondition. This concludes the proof of termination of the original program. Note that the unfolding/narrowing mechanism provides not only a termination proof but also a characterization of the program execution phases. In particular, our example can be viewed to have three phases, corresponding to the unfoldings we have applied. One phase corresponds to the case where z < 0 (where the else -block is repeatedly used), one to the case z > 0 ∧x < 0, and finally, one corresponds to the case z > 0∧x≥0.  To formalize this execution phase-structured proof technique, we first define the unfolding program transformation: Definition 4. Let P be a program, C a component of P , EC its entry transitions, XC its exit transitions, and Q : L ( C ) →F ( V )a conditional invariant for C . The unfolding of Pis b P={(`s, ρ ∧¬Q(`t)0, `t), (`s, ρ ∧ Q(`t)0,b `t), (b `s, ρ ∧ Q(`s),b `t)|(`s, ρ, `t)∈ C } ∪ { (`s, ρ ∧ ¬Q(`t)0, `t), (`s, ρ ∧ Q(`t)0,b `t)|(`s, ρ, `t)∈ EC} ∪ { (`s, ρ, `t), (b `s, ρ, `t)|(`s, ρ, `t)∈ XC} ∪ {τ|τ∈ P \(C ∪ EC∪ XC)} 16 C. Borralleras et al. References 1. E. Albert, P. Arenas, M. Codish, S. Genaim, G. Puebla, and D. Zanardini. Termination analysis of Java Bytecode. In FMOODS, 2008. 2. C. Alias, A. Darte, P. Feautrier, and L. Gonnord. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In SAS, 2010. 3. R. Bagnara, F. Mesnard, A. Pescetti, and E. Zaffanella. A new look at the automatic synthesis of linear ranking functions. IC, 215, 2012. 4. A. Bakhirkin and N. Piterman. Finding recurrent sets with backward analysis and trace partitioning. In TACAS, 2016. 5. A. M. Ben-Amram and S. Genaim. On the linear ranking problem for integer linear-constraint loops. In POPL, 2013. 6. A. Biere, M. J. H. Heule, H. van Maaren, and T. Walsh, editors. Handbook of Satisfiability. IOS Press, 2009. 7. M. Bozga, R. Iosif, and F. Konecn´y. Deciding conditional termination. LCMS, 10(3), 2014. 8. A. R. Bradley, Z. Manna, and H. B. Sipma. Linear ranking with reachability. In CAV, 2005. 9. M. Brockschmidt, B. Cook, and C. Fuhs. Better termination proving through cooperation. In CAV, 2013. 10. M. Brockschmidt, B. Cook, S. Ishtiaq, H. Khlaaf, and N. Piterman. T2: temporal property verification. In TACAS, 2016. 11. M. Brockschmidt, S. J. Joosten, R. Thiemann, and A. Yamada. Certifying safety and termination proofs for integer transition systems. In WST, 2016. 12. M. Brockschmidt, D. Larraz, A. Oliveras, E. Rodr´ıguez-Carbonell, and A. Rubio. Compositional safety verification with max-smt. In FMCAD, 2015. 13. M. Brockschmidt, T. Str¨oder, C. Otto, and J. Giesl. Automated detection of non-termination and NullPointerExceptions for JBC. In FoVeOOS, 2011. 14. H. Y. Chen, B. Cook, C. Fuhs, K. Nimkar, and P. W. O’Hearn. Proving nontermination via safety. In TACAS, 2014. 15. B. Cook, S. Gulwani, T. Lev-Ami, A. Rybalchenko, and M. Sagiv. Proving conditional termination. In CAV, 2008. 16. B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In PLDI, 2006. 17. V. D’Silva and C. Urban. Conflict-driven conditional termination. In CAV, 2015. 18. S. Falke, D. Kapur, and C. Sinz. Termination analysis of Cprograms using compiler intermediate languages. In RTA, 2011. 19. S. Falke, D. Kapur, and C. Sinz. Termination analysis of imperative programs using bitvector arithmetic. In VSTTE, 2012. 20. A. Flores-Montoya and R. H¨ahnle. Resource analysis of complex programs with cost equations. In APLAS, pages 275–295, 2014. 21. P. Ganty and S. Genaim. Proving termination starting from the end. In CAV, 2013. 22. J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Pl¨ucker, P. Schneider-Kamp, T. Str¨oder, S. Swiderski, and R. Thiemann. Analyzing program termination and complexity automatically with AProVE.JAR, 2016. To appear. 23. L. Gonnord, D. Monniaux, and G. Radanne. Synthesis of ranking functions using extremal counterexamples. In PLDI, 2015. 24. A. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, and R.-G. Xu. Proving non-termination. In POPL, 2008. Proving Termination through Conditional Termination 17 25. W. R. Harris, A. Lal, A. V. Nori, and S. K. Rajamani. Alternation for termination. In SAS, 2010. 26. M. Heizmann, J. Hoenicke, and A. Podelski. Termination analysis by learning terminating programs. In CAV, 2014. 27. C. Kop and N. Nishida. Constrained term rewriting tool. In LPAR-20, 2015. 28. D. Kroening, N. Sharygina, A. Tsitovich, and C. M. Wintersteiger. Termination analysis with compositional transition invariants. In CAV, 2009. 29. D. Larraz, K. Nimkar, A. Oliveras, E. Rodr´ıguez-Carbonell, and A. Rubio. Proving non-termination using Max-SMT. In CAV, 2014. 30. D. Larraz, A. Oliveras, E. Rodr´ıguez-Carbonell, and A. Rubio. Proving termination of imperative programs using Max-SMT. In FMCAD, 2013. 31. D. Larraz, A. Oliveras, E. Rodr´ıguez-Carbonell, and A. Rubio. Minimal-modelguided approaches to solving polynomial constraints and extensions. In SAT, 2014. 32. T. C. Le, S. Qin, and W. Chin. Termination and non-termination specification inference. In PLDI, 2015. 33. J. Leike and M. Heizmann. Ranking templates for linear loops. In TACAS, 2014. 34. D. Mass´e. Policy iteration-based conditional termination and ranking functions. In VMCAI, 2014. 35. A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI, 2004. 36. A. Podelski and A. Rybalchenko. ARMC: The logical choice for software model checking with abstraction refinement. In PADL, 2007. 37. R. Sharma, I. Dillig, T. Dillig, and A. Aiken. Simplifying loop invariant generation using splitter predicates. In CAV, 2011. 38. M. Sinn, F. Zuleger, and H. Veith. A simple and scalable static analysis for bound analysis and amortized complexity analysis. In CAV, pages 745–761, 2014. 39. F. Spoto, F. Mesnard, and ´ E. Payet. A termination analyser for Java Bytecode based on path-length. TOPLAS, 32(3), 2010. 40. A. Stump, G. Sutcliffe, and C. Tinelli. Starexec: a cross-community infrastructure for logic solving. In IJCAR, 2014. 41. Termination Competition. http://termination-portal.org/wiki/Termination_ Competition. 42. A. Tsitovich, N. Sharygina, C. M. Wintersteiger, and D. Kroening. Loop summarization and termination analysis. In TACAS, 2011. 43. C. Urban. The abstract domain of segmented ranking functions. In SAS, 2013. 44. C. Urban, A. Gurfinkel, and T. Kahsai. Synthesizing ranking functions from bits and pieces. In TACAS, 2016. 45. C. Urban and A. Min´e. A decision tree abstract domain for proving conditional termination. In SAS, 2014. 46. H. Velroyen and P. R¨ummer. Non-termination checking for imperative programs. In TAP, 2008.