AProVE (KoAT + LoAT)

AProVE (KoAT + LoAT) is a framework combining our three tools AProVE, KoAT, and LoAT to prove or disprove termination of C programs automatically. To this end, the C program is compiled into the intermediate representation of the LLVM framework [28] by the Clang compiler [1]. Afterwards, the LLVM program is processed by AProVE and transformed into a symbolic execution graph (SEG, see [24, 26, 36, 37] for more details). Finally, the SEG is either analyzed directly by AProVE (see [23‐25, 37] for more details on the internal (non-)termination proofs in AProVE) or transformed into integer transition systems (ITSs). These ITSs are analyzed by our tools KoAT [8, 20, 29‐32] (for termination) and LoAT [14‐17] (for non-termination). In case of non-termination, the proofs by AProVE and LoAT are transformed into non-termination proofs for the original C program.

Earlier versions of AProVE that participated in SV-COMP until 2022 used the external tool T2 [7] for proving termination of ITSs (and both T2 and LoAT for proving non-termination). In contrast, instead of T2, our new version uses our own ITS analyzer KoAT in the backend which allows us to benefit from the numerous recent improvements that we developed for KoAT. A bird’s-eye view of our approach is sketched in Fig. 1.

Termination Analysis by KoAT: In the following, we briefly describe how our tool KoAT proves termination of ITSs which result from the transformation of \(\textsf {C}\) programs. LoAT can be used to disprove termination and infer lower runtime bounds for ITSs, and its integration in order to prove non-termination of \(\textsf {C}\) programs was described in [25]. In contrast, KoAT is a tool to automatically prove termination and infer upper complexity bounds for ITSs based on a modular analysis of separate program parts [8, 32]. To prove termination of sub-programs, it uses multiphase-linear ranking functions (M\(\varPhi \)RFs) [5, 20]. In contrast to classical ranking functions, M\(\varPhi \)RFs can also represent bounds on programs with multiple “phases” of executions.

Moreover, we embedded a technique [21] to analyze termination of so-called triangular weakly non-linear loops (twn-loops) in our tool KoAT [29, 32]. In particular, this approach also allows us to analyze programs with non-linear arithmetic. An example for a terminating twn-loop, which may result from a sub-program within a larger C program, is:This loop does not admit a M\(\varPhi \)RF over \(\mathbb {R}\) (see [22]). The guard of such twn-loops are propositional formulas over (possibly non-linear) polynomial inequations. The update is triangular, i.e., we can order the variables such that the update of any \(x_i\) does not depend on the variables \(x_1, \ldots , x_{i-1}\) with smaller indices. So the restriction to triangular updates prohibits “cyclic dependencies” of variables (e.g., where the new values of \(x_1\) and \(x_2\) both depend on the old values of \(x_1\) and \(x_2\)). For example, a loop whose body consists of the assignment \((x_1, x_2) \leftarrow (x_1 + x_2^2, x_2+1)\) is triangular, whereas a loop with the body \((x_1, x_2) \leftarrow (x_1 + x_2^2, x_1+1)\) is not triangular. From a practical point of view, the restriction to triangular loops seems quite natural. For example, in [15], 1511 polynomial loops were extracted from the Termination Problems Data Base [38], the benchmark collection which is used at the annual Termination and Complexity Competition [19], and only 26 of them were non-triangular. Furthermore, the update of a twn-loop is weakly non-linear, i.e., no variable \(x_i\) has a non-linear occurrence in its own update. So for example, a loop with the body \((x_1, x_2) \leftarrow (x_1 +x_2^2, x_2+1)\) is weakly non-linear, whereas a loop with the body \((x_1, x_2) \leftarrow (x_1 \cdot x_2, x_2+1)\) is not. With triangularity and weak non-linearity, one can compute a closed form which corresponds to applying the loop’s update n times. For example, the closed forms of (1) are \(x_1 \cdot 4^n\), \((x_2 - x_3^3) \cdot 9^n + x_3^3\), and \(x_3\) for \(x_1\), \(x_2\), and \(x_3\), respectively.

Using these closed forms, termination can be reduced to a formula over \(\mathbb {Z}\) [21] (whose satisfiability is decidable for linear arithmetic and where SMT solvers often also prove (un)satisfiability in the non-linear case). The idea of the reduction is to consider each atom of the loop guard individually, instantiate the variables in the atoms by their closed forms, and order the summands of the resulting expressions w.r.t. their growth rate in n. For example, for the atom \(x_2 - x_1^2 > 0\) of (1), we obtain \(\alpha _1 \cdot 16^n + \alpha _2 \cdot 9^n + \alpha _3 > 0\) where \(\alpha _1 = - x_1^2\), \(\alpha _2 = x_2 - x_3^3\), and \(\alpha _3 = x_3^3\). If the initial values of the variables satisfy \(\alpha _1 > 0\), then the addend \(\alpha _1 \cdot 16^n\) would dominate all other addends at some point and the atom \(x_2 - x_1^2 > 0\) would hold for all large enough n, assuming that there are no overflows. (However, in our example \(\alpha _1 = -x_1^2 > 0\) is unsatisfiable.) Otherwise, if \(\alpha _1 = -x_1^2 = 0\), then the second addend \(\alpha _2 \cdot 9^n\) is the fastest growing summand. Applying this idea to all addends subsequently, i.e., checking if the first polynomials \(\alpha _1, \ldots , \alpha _{j-1}\) are 0 and \(\alpha _j\) is positive, we can reduce non-termination to an existential first-order (FO) problem. For our example, we obtain the reduction \({{\,\textrm{red}\,}}(x_2 - x_1^2 > 0) = \alpha _1 > 0 \vee (\alpha _1 = 0 \wedge \alpha _2 > 0) \vee (\alpha _1 = 0 \wedge \alpha _2 = 0 \wedge \alpha _3 > 0)\) for the atom \(x_2 - x_1^2 > 0\). Similarly, we have \({{\,\textrm{red}\,}}(x_1 > 0) = (x_1 > 0)\) for the second atom of the loop guard. Replacing the atoms of the guard by their reduction results in the overall FO problem \(\psi = {{\,\textrm{red}\,}}(x_2 - x_1^2 > 0) \wedge {{\,\textrm{red}\,}}(x_1 > 0)\). Thus, (1) is non-terminating over \(\mathbb {Z}\) iff \(\psi \) is satisfiable over \(\mathbb {Z}\). In our example, the formula \(\psi \) is unsatisfiable since \({{\,\textrm{red}\,}}(x_2 - x_1^2 > 0)\) is only satisfiable if \(x_1 = 0\). However, this violates \({{\,\textrm{red}\,}}(x_1 > 0)\). Thus, the twn-loop (1) is terminating.

KoAT’s novel approach of analyzing some sub-programs with ranking functions and other sub-programs with our technique for twn-loops increases the power of automated termination analysis substantially, in particular also for programs containing non-linear arithmetic. Nevertheless, there still exist programs whose termination is difficult to analyze and where it would help to gain “more information” on the values of variables in order to determine the infeasibility of certain paths in the program. For example, one could transform a loop whose body contains an if-else-instruction where either always the if-branch or the else-branch are executed into two separate single-path loops. This transformation explicitly removes infeasible paths which contain both branches. Thus, the idea is to transform an ITS \(\mathcal {P}\) into a new ITS \(\mathcal {P}'\) which is “easier” to analyze. Of course, we ensure that the runtime of \(\mathcal {P}'\) is at least the runtime of \(\mathcal {P}\). Then it is sound to prove termination for \(\mathcal {P}'\) instead of \(\mathcal {P}\). Such transformations can be performed by control-flow refinement via partial evaluation [11], which we integrated into KoAT’s approach [20, 31].

An underlying design concept of AProVE (KoAT + LoAT) is its modular structure. It allows us to use different backends and techniques to analyze programs and benefit from their individual strengths. Hence, our new framework can make use of recent progress in software verification tools. Furthermore, both AProVE and our backend tools KoAT and LoAT are modular themselves (see, e.g., KoAT’s modular analysis of sub-programs in Sect. 1).

One of AProVE’s main weaknesses was that it essentially relied on variants of (linear) ranking functions for termination proofs. However, this problem has now been solved by integrating our tool KoAT into AProVE. Besides ranking functions, KoAT also uses a technique for termination analysis of twn-loops which allows us to analyze programs with non-linear arithmetic on which the other soundtools participating in the termination category of SV-COMP fail. For example, the C program which just instantiates all variables non-deterministically and consists of the loop (1) and even its following linear, simplified variant from [22]can both not be shown terminating by Ultimate Automizer [10] and 2LS [35], which were the two most powerful sound¹ tools at the termination category of last year’s SV-COMP. In contrast, AProVE proves their termination using the implementation of our termination technique for twn-loops in KoAT.

Concerning the proofs of non-termination, currently AProVE (KoAT + LoAT) uses a version of LoAT which disproves termination using the loop acceleration technique of [16]. In [17], a new version of LoAT was developed that is based on an acceleration driven clause learning calculus which improves LoAT’s power for non-termination proofs substantially. We plan to integrate this new version in our AProVE (KoAT + LoAT) framework in the future, using a new format to ease the automated handling of LoAT’s non-termination proofs. Moreover, as KoAT and LoAT can also analyze complexity of programs, it would be interesting to extend AProVE (KoAT + LoAT) to complexity analysis as well.

AProVE (KoAT + LoAT) is developed in the “Programming Languages and Verification” group at RWTH Aachen University. A list of present and past contributors can be accessed on the website [2]. In SV-COMP 2025, AProVE (KoAT + LoAT) only participates in the category “Termination”. All files from the submitted archive [33] must be extracted into one folder. AProVE is implemented in Javaand needs a Java 17 Runtime Environment. To analyze the resulting ITSs in the backend, the tools KoAT [20, 29‐32] and LoAT [14‐17] are used. Furthermore, it applies the satisfiability checkers Z3 [9], Yices [12], and MiniSAT [13], see [18].Our archive contains all these tools. Using the wrapper script aprove.py in theBenchExec repository, AProVE (KoAT + LoAT) can be invoked, e.g., on the benchmarks defined in aprove.xml in the SV-COMP repository. The most recentversion of our tool for SV-COMP 2025 [6] can be downloaded at [33]. Moreover, \(\textsf {C}\) programs for all examples from the paper are available at [33] and [34].