arXiv CSopen access

Loop-Based Slicing and Input-Driven Concretization: An Empirical Study of Termination and Non-Termination Analysis

1

Loop-Based Slicing and Input-Driven Concretization: An Empirical Study of Termination and Non-Termination Analysis

arXiv:2607.08988v1 [cs.SE] 9 Jul 2026

Negar Fathi, Rahul Purandare, Tachio Terauchi, and Hiroshi Unno

Abstract—Termination and non-termination are fundamental correctness properties, but verifying them in real-world C programs remains difficult because loop interactions and nondeterministic inputs challenge existing analyzers. This paper presents an empirical study of lightweight, tool-independent source-level preprocessing for (non-)termination analysis. We implement F OCUS TNT, a C front end that applies loop-based slicing to isolate loop-level obligations and input-driven concretization to specialize nondeterministic inputs into selected input-scenario variants. We evaluate slicing, concretization, and their combination across six analyzers on 117 C/C++ programs derived from real-world non-termination bugs and their fixes. The study examines effects on analyzer correctness, complementarity with original-program analysis, loop-level diagnostics, feature sensitivity, runtime behavior, semantic scope, and integration potential. Results show that preprocessing is not uniformly beneficial: its impact depends on the analyzer, task, and program features. Slicing provides conservative structural isolation and localization, whereas concretization can improve detectability for selected scenarios but narrows semantic scope and may increase analysis effort. Their combination is not consistently additive. Overall, the results support adaptive use of preprocessing as a complement to original-program analysis and provide practical guidance to application developers interpreting verification outcomes and tool developers improving analyzer robustness. Index Terms—Termination Analysis, Non-Termination Analysis, Program Slicing, Concretization, Program Preprocessing, Empirical Evaluation.

I. I NTRODUCTION Termination and non-termination are fundamental correctness properties in program analysis, especially for systems software where infinite execution can compromise responsiveness and reliability [1], [2]. Failure to establish termination can also obstruct verification tasks that assume eventual return, such as liveness reasoning and compositional arguments [1]. In practice, proving (non-)termination remains difficult because loops are often embedded in large, semantically noisy contexts that obscure the statements and dependencies most relevant to termination behavior [1], [2]. Environment-driven nondeterminism further complicates analysis by exposing many inputdependent behaviors, only some of which may matter for a particular (non-)termination outcome [3], [4], [2]. N. Fathi and R. Purandare are with the University of Nebraska– Lincoln, Lincoln, NE, USA. Email addresses: [email protected], [email protected]. T. Terauchi is with Waseda University, Tokyo, Japan. Email: [email protected]. H. Unno is with Tohoku University, Sendai, Japan. Email: [email protected].

Static analyzers address termination properties by constructing proofs that generalize across executions, combining abstraction [5], [6], invariant inference [7], [8], [9], rankingfunction synthesis [10], [11], [8], [12], [13], recurrence reasoning [14], [15], [4], [6], and solver-based back ends [4], [3], [9]. Although such tools perform well on established benchmarks such as TermCOMP [16] and SV-COMP [17], prior studies show that they still struggle on programs derived from real-world non-termination bugs, where complex program context, nondeterministic inputs, and C/C++-specific features make proof construction difficult [18], [19]. Dynamic approaches complement static analysis by using concrete executions to expose input-specific (non-)termination behaviors and generate witnesses when divergence depends on particular input patterns [20], [21], [22]. However, execution evidence alone cannot establish general termination guarantees, since observing termination on finitely many executions does not imply termination of all executions [20], [22]. This paper studies (non-)termination analysis from a preprocessing perspective: rather than proposing a new termination prover, we ask whether lightweight source-level transformations can reshape verification tasks before they reach existing analyzers. We focus on two transformations motivated by the challenges above: loop-based slicing, which isolates loop-relevant structure while preserving the analyzed loop’s termination behavior, and input-driven concretization, which specializes nondeterministic inputs into selected input-scenario variants. These transformations may help analyzers focus on loop-relevant dependencies or reason about restricted inputdependent behaviors, but they may also remove useful context, expose different behaviors, or narrow semantic scope; their effects therefore require empirical evaluation. We implement this perspective in F OCUS TNT, a lightweight, tool-independent preprocessing front end for C programs that supports loop-based slicing and input-driven concretization. We evaluate four configurations—BASE (no preprocessing), S LICE (slicing only), C NCRT (concretization only), and S LICE +C NCRT (slicing followed by concretization)—across six analyzers: Athena [23], Proton [24], [25], UAutomizer [26], AProVE [27], CPAchecker [28], and 2LS [29]. Our study uses 117 C/C++ programs derived from real-world non-termination bugs and their fixes [18], [30] and examines analyzer correctness, complementarity with original-program analysis, loop-level diagnostics, feature sensitivity, runtime behavior, semantic scope, and integration potential. These dimensions

2

provide practical insight for application developers interpreting preprocessing-based verification outcomes and tool developers improving analyzer robustness. In summary, this work makes the following contributions: 1) We design and implement F OCUS TNT, a lightweight, tool-independent C preprocessing framework that supports loop-based slicing, input-driven concretization, and their combination without modifying backend analyzers. 2) We conduct a multi-tool empirical evaluation of four configurations—BASE, S LICE, C NCRT, and S LICE +C NCRT—across six termination and nontermination analyzers on 117 C/C++ programs derived from real-world non-termination bugs and their fixes. 3) We assess preprocessing effects on analyzer correctness, complementarity with original-program analysis, loop-level diagnostics, feature sensitivity, runtime behavior, semantic scope, and integration potential. 4) We derive practical implications for adaptive preprocessing, helping application developers interpret preprocessingbased verification outcomes and tool developers identify feature- and transformation-sensitive cases for improving analyzer robustness. The remainder of the paper is organized as follows. Section II presents motivating examples. Section III reviews related work. Sections IV and V introduce the preprocessing framework and implementation. Sections VI and VII define the experimental setup and present the empirical results. Section VIII discusses the main findings and implications, Section IX examines threats to validity, and Section X concludes with future work. II. M OTIVATING E XAMPLES Shi et al. [18], [30] introduced a benchmark of simplified C/C++ programs derived from real-world non-termination bugs and their fixes. We use two representative cases to illustrate how loop-based slicing and input-driven concretization reshape verification tasks: Misusing_Variable_Type_1_NT (Figure 1) and Incorrect_Control_Statement_2_NT (Figure 2). Figure 1a shows a program with three nested unsignedinteger loops. The two decrementing loops are non-terminating because unsigned wrap-around keeps their guards satisfiable, while the innermost loop is bounded and terminating. Under BASE, analyzers must reason about one program coupling all three loop variables and control structure: only Athena and 2LS prove non-termination, UAutomizer, AProVE, and CPAchecker are inconclusive, and Proton incorrectly reports termination. Loop-based slicing (Section IV-B) decomposes the program into loop-centric variants (Figures 1b, 1c, and 1d), each preserving the termination behavior relevant to one loop. This isolates loop-local reasoning tasks and reduces interference from surrounding loops. On these slices, previously inconclusive analyzers prove termination of the bounded inner loop and non-termination of at least one diverging loop, while Proton no longer reports termination and instead becomes inconclusive. Under the aggregation policy in Algorithm 1, detecting one non-terminating slice suffices to classify the

1 2 3 4 5 6 7 8

int main() { unsigned int mul, div1, div2; for(div1 = 1; div1 >= 0; div1--) { for(div2 = 7; div2 >= 0; div2--) { for(mul = 0; mul <= 255; mul++) { }}} return 0; }

(a) Original program. 1 2 3 4 5

void main(void) { unsigned int div1; div1 = (unsigned int)1; while (div1 >= (unsigned int)0) div1--; }

(b) Outer-loop slice. 1 2 3 4 5

void main(void) { unsigned int div2; div2 = (unsigned int)7; while (div2 >= (unsigned int)0) div2--; }

(c) Middle-loop slice. 1 2 3 4 5

void main(void) { unsigned int mul; mul = (unsigned int)0; while (mul <= (unsigned int)255) mul++; }

(d) Inner-loop slice.

Fig. 1: Motivating example for loop-based slicing: Misusing_Variable_Type_1_NT, from Shi et al.’s benchmark suite [18], [30].

original non-terminating benchmark correctly. Thus, all analyzers except Proton reach a correct program-level conclusion under slicing, and Proton’s earlier incorrect termination result is eliminated. This example shows how slicing localizes divergence reasoning and exposes loop-specific behavior obscured in the original program. Figure 2 shows a program whose loop behavior depends on arrays initialized with __VERIFIER_nondet_int(). The counter i advances only on some control-flow paths: if slots_used[i] repeatedly takes a particular value, execution bypasses the increment of i, preventing progress and causing non-termination; otherwise, i eventually increases and the loop terminates. Under BASE, analyzers must reason about both terminating and diverging behaviors induced by nondeterministic inputs: Proton and UAutomizer prove nontermination, AProVE and 2LS are inconclusive, Athena times out, and CPAchecker reports an error. Input-driven concretization (Section IV-C) specializes nondeterministic inputs by instantiating slots_used and ereg with concrete values derived from candidate inputs discovered and validated by the procedure described in that section. The resulting variants restrict analysis to selected input-scenario behaviors, reducing nondeterministic variability and making input-specific termination or divergence easier to expose. After concretization, Athena and 2LS, which did not resolve the original program, resolve several specialized variants, including some classified as non-terminating. Under the aggregation policy in Algo-

3

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29

extern int __VERIFIER_nondet_int(void); #define EVEBT_EPOLL_SLOTS 2 int main() { int EVENT_EPOLL_TABLES = 10; int slots_used[10]; int ereg[10]; int table; for (int i = 0; i < 10; i++) { slots_used[i] = __VERIFIER_nondet_int(); ereg[i] = __VERIFIER_nondet_int(); } int i = 0; while (i < EVENT_EPOLL_TABLES) { switch (slots_used[i]) { case EVEBT_EPOLL_SLOTS: continue; case 0: if (!ereg[i]) return 0; else table = ereg[i]; break; default: table = ereg[i]; break; } if (table) break; i++; } return 0; }

Fig. 2: Motivating example for input-driven concretization: Incorrect_Control_Statement_2_NT, from Shi et al.’s benchmark suite [18], [30].

rithm 1, the non-terminating variant results suffice for a correct overall non-termination classification. This example shows how input-driven concretization complements static reasoning by presenting analyzers with restricted execution domains. Together, these examples show that preprocessing can reshape verification tasks without changing backend analyzers. Loop-based slicing isolates loop structure while preserving its termination behavior, whereas input-driven concretization restricts nondeterministic variability to selected input scenarios. These transformations expose alternative verification views with distinct semantic effects, motivating our empirical study of their benefits, limitations, and interactions across analyzers. III. R ELATED W ORK We position our work with respect to program slicing and static, dynamic, and hybrid approaches to (non-)termination analysis. a) Program Slicing: Program slicing extracts components relevant to a slicing criterion, such as selected variable values at a program point [31]. Static slicing over-approximates behavior across executions, whereas dynamic slicing is tied to a concrete execution and produces a trace-specific slice that may not generalize beyond the observed run [31], [32]. Several infrastructures support C/C++ slicing at the source or intermediate representation (IR) level: CodeSurfer [33] builds system dependence graphs for forward and backward slicing and chopping queries; Frama-C [34] provides sourcelevel slicing integrated with abstract interpretation; DG [35] performs dependence-graph-based slicing over LLVM bitcode;

and Giri [36] performs dynamic backward slicing from execution traces. Prior work has used slicing mainly for debugging, program comprehension, and verification reduction. In contrast, we use loop-based slicing as a verification-oriented structural isolation step for (non-)termination analysis. Our C sourcelevel implementation uses Frama-C [34], avoiding IR-level translation and potential decompilation issues while remaining compatible with existing termination analyzers. b) Static (Non-)Termination Analysis: Termination and non-termination analysis for imperative programs is predominantly static and proof-oriented, aiming to establish guarantees that generalize across executions. We briefly describe the stateof-the-art C analyzers used in our study, which represent different verification paradigms. Athena [23] is a sound C (non-)termination analyzer that models low-level semantics using pointer-to-array rewriting and bit-precise bounded-integer reasoning. It translates programs into logical transition systems and applies µCLP solving in the MuVal primal–dual fixpoint framework [37], [38], [39], synthesizing ranking functions and recurrent sets through mutually recursive inductive and co-inductive predicates. Proton [24], [25] detects non-termination by finding recurrent program states with bounded model checking and supports termination analysis through LLM-assisted candidate ranking functions validated by randomized testing and bounded model checking. UAutomizer [40], [26], [41], [42], [43] is an automata-based verifier using trace abstraction and interpolation-based refinement, with (non-)termination reasoning over infinite traces and lasso-shaped executions. AProVE [27], [44], [45], [46] builds symbolic execution graphs that over-approximate executions and translates them into integer transition or rewrite systems for automated (non)termination analysis. CPAchecker [28] is a configurable verification framework that performs reachability analysis over control-flow automata by combining abstract domains such as predicate abstraction and explicit-value analysis. 2LS [29], [47], [48], [49] is a bit-precise CPROVER-based analyzer combining bounded model checking, k-induction, and template-based invariant synthesis for interprocedural termination and non-termination analysis over bitvector semantics. Our work is complementary to these analyzers: rather than modifying their reasoning engines or adding proof rules, we treat them as black boxes and study how lightweight source-level preprocessing reshapes their verification tasks. This enables an empirical analysis of when preprocessing helps or hurts, and how its effects depend on analyzer architecture, program features, and the termination versus nontermination task. The findings help application developers interpret preprocessing-based outcomes and tool developers improve analyzer robustness. c) Dynamic and Hybrid (Non-)Termination Analyses: Dynamic and hybrid approaches complement static reasoning by using concrete executions to expose or explain termination behavior. DynamiTe [20] collects traces, learns candidate ranking functions and recurrent sets, and validates them with SMTbased static reasoning, using failed validations to drive further executions in a dynamic–static refinement loop. FuzzNT [21]

4

Fig. 3: Overview of the F OCUS TNT preprocessing and verification pipeline.

combines coverage-guided fuzzing with a guess-and-check workflow that builds path-specialized under-approximating variants, analyzed by abstract interpretation to confirm nontermination. EndWatch [22] targets real-world software by instrumenting loops with state-revisit non-termination oracles and exploring executions via fuzzing and symbolic execution. Our input-driven concretization is related to these hybrid approaches because it uses concrete input scenarios to specialize analysis tasks. However, rather than building a new dynamic– static verification engine, we externalize specialization as source-level preprocessing and evaluate how the resulting variants affect existing analyzers. Combined with loop-based slicing, this lets us study structural isolation and input-scenario specialization as complementary preprocessing dimensions for (non-)termination analysis and guides their integration into verification workflows. IV. A PPROACH This section presents F OCUS TNT, the source-level preprocessing pipeline underlying our empirical study. A. Pipeline Overview Figure 3 gives an overview of the F OCUS TNT preprocessing pipeline. The pipeline takes as input a C program and a tabular input specification whose columns identify nondeterministic input locations and whose rows define concrete input assignments. The first stage optionally applies loopbased slicing and produces N program variants. If slicing is disabled, this stage produces the original program (N = 1); if the program has a single loop, it produces one sliced variant (N = 1); and if the program has multiple loops, it produces N > 1 loop-focused sliced variants. The second stage optionally applies input-driven concretization. If concretization is disabled, the current N variants are analyzed unchanged (M = 1); otherwise, each variant is specialized using M > 1 selected input assignments, yielding M × N concretized variants. Each generated variant is analyzed independently by off-the-shelf termination and non-termination tools, which return one of yes, no, unknown, timeout, error. Algorithm 1 evaluates the resulting outcomes against program- and variant-level ground truth, producing a program-level decision (correct or wrong)

and the fractions of terminating and non-terminating variants correctly classified, denoted ratioT and ratioN T . B. Loop-Based Slicing The loop-based slicing phase isolates each syntactic loop in a separate program variant. Given a program P , F OCUS TNT generates one slice per loop, retaining the code required by the slicing criterion to preserve termination-relevant behavior for that loop while removing unrelated variables, statements, and functions when possible. This gives analyzers a smaller, more focused verification task with less interference from surrounding context. The resulting slices are loop-focused variants interpreted relative to the selected loop and slicing criterion, not claims of whole-program semantic equivalence. In particular, the current slicing procedure targets syntactic loop obligations rather than recursive call cycles. Accordingly, it does not introduce separate slicing criteria or recursionfocused variants for recursive code; such code is considered only insofar as it contributes to the context of a selected loop and the dependences captured by its slicing criterion. For each for, while, or do–while loop ℓ in P , F O CUS TNT uses the Clang [50] abstract syntax tree to construct a loop descriptor
D(ℓ) = loc(ℓ), func(ℓ), Tcond (ℓ), Sctrl (ℓ) , where: • loc(ℓ) is the source location of ℓ. • func(ℓ) is the function enclosing ℓ. • Tcond (ℓ) is the set of lvalues in the loop guard. An lvalue denotes a memory location, such as a scalar variable, array element, or field access. Scalars are recorded directly, while array and field accesses are abstracted to their base memory objects to conservatively capture dependences. • Sctrl (ℓ) is the set of source locations of loop-control statements in the loop body, including continue, break, goto, and return. The descriptor induces the loop-local slicing criterion C(ℓ) = Read(Tcond (ℓ)) ∪ Annotate(Sctrl (ℓ)) , where Read(·) denotes reads of guard-relevant lvalues and Annotate(·) denotes ANSI/ISO C Specification Language

5

(ACSL) annotations inserted at the recorded loop-control locations. Operationally, F OCUS TNT encodes this criterion as Frama-C [34] slicing directives over the selected guard reads and annotated loop-control locations. Frama-C then retains statements needed to preserve the associated data and control dependences. Loops in main and auxiliary functions are handled differently. If ℓ appears in main, F OCUS TNT invokes Frama-C with main as the entry point and slices directly with respect to C(ℓ), producing Slice(P, ℓ). For loops in non-main functions, F OCUS TNT constructs two slices. The callee-focused slice is rooted at func(ℓ) and uses the criterion C(ℓ) ∪ KeepReturn(func(ℓ)) , where KeepReturn(·) is the Frama-C directive used to retain the return behavior of the enclosing function. The callerfocused slice is rooted at main and uses KeepCalls(func(ℓ)) , where KeepCalls(·) retains calls to func(ℓ) along the invocation context rooted at main. The final slice Slice(P, ℓ) replaces the corresponding function body in the caller-focused slice with the callee-focused reduced version, retaining the relevant invocation context while keeping the generated program focused on ℓ. C. Input-Driven Concretization The input-driven concretization phase specializes nondeterministic inputs for selected input scenarios. Given a program variant from the previous stage and a tabular input specification, it produces one concretized variant per input assignment by replacing nondeterministic input generators with typecorrect concrete values. By reducing nondeterministic variability, concretization can make input-dependent termination or divergence easier to expose. The resulting variants represent selected input-scenario behaviors and therefore do not cover all executions of the original program. Concrete inputs are specified as a table whose header contains N identifiers h1 , h2 , . . . , hN and whose M rows define individual input assignments. Each identifier has the form hi = xi :: fi :: ki 1 ≤ i ≤ N, where xi is the assigned lvalue expression when a corresponding __VERIFIER_nondet_*() call appears on the righthand side of an initialization or assignment, and the reserved token NONDET otherwise; fi is the enclosing function; and ki ∈ N distinguishes syntactic occurrences within the function by source order. Each row defines an assignment tj = {h1 7→ cj1 , h2 7→ cj2 , . . . , hN 7→ cjN }

1 ≤ j ≤ M,

where each cji is a type-correct concrete literal assigned to hi . The resulting input set is denoted T = t1 , t2 , . . . , tM . Given a program variant P and input assignment t ∈ T , the concretized program Cncrt(P, t) specializes every nondeterministic call in P according to t. Each call is mapped to its identifier h = x :: f :: k and rewritten by replacing the

call expression with the literal c = t(h) while preserving the surrounding expression context. We assume the input specification assigns values to all identifiers, so nondeterministic inputs are fully specialized. In the current implementation, repeated evaluations of the same syntactic nondeterministic call within one execution, including inside loops, use the same concrete value. Concretization is an intentional under-approximation: Cncrt(P, t) restricts P to executions consistent with a selected input assignment t, rather than representing all nondeterministic choices. Thus, termination of Cncrt(P, t) holds only for that input scenario and does not imply universal termination of P . Conversely, if Cncrt(P, t) is non-terminating and t is feasible for P , it witnesses non-termination of the original program. Concretization can therefore expose input-dependent behavior more effectively, but its conclusions must be interpreted with respect to the selected assignments. We implement concretization as a Clang-based source-to-source transformation that generates one variant for each pair (P, t); if concretization is disabled or no input specification is provided, the program is analyzed unchanged. Input generation is not a contribution of this work. Input assignments are used only to instantiate selected scenarios for evaluating input-driven concretization. We construct input sets through controlled candidate discovery followed by manual validation. For each benchmark, OpenAI’s ChatGPT (GPT-4o) proposes candidate assignments, which are then curated by discarding inconsistent cases and refining execution scenarios into a fixed set of feasible assignments, including both terminating and diverging scenarios when available. This LLM-assisted step is only a practical mechanism for obtaining diverse assignments: the model is not treated as an oracle and is not used to establish ground truth. We also evaluated automated generators such as KLEE [51] and AFL [52], but complex C features and timeout-truncated diverging executions often limited the usefulness of automatically derived witnesses in our setting. D. Termination and Non-Termination Verification We evaluate four analysis configurations that differ only in preprocessing before verification: BASE (no preprocessing), S LICE (loop-based slicing only), C NCRT (input-driven concretization only), and S LICE +C NCRT (slicing followed by concretization). These configurations isolate the individual and combined effects of loop-level structural isolation and inputscenario specialization while keeping backend analyzers and the verification workflow unchanged. The combined configuration, S LICE +C NCRT, is included to study interactions between slicing and concretization, not as a prescribed deployment strategy. Under each configuration, the pipeline generates one or more program variants from the same original program. Each variant is analyzed independently by the selected off-theshelf termination and non-termination tools. Each analyzer invocation returns one of yes, no, unknown, timeout, error: yes denotes a termination proof, no a non-termination proof, unknown an inconclusive result within the time limit, timeout

6

Algorithm 1: Program-Level Tool Decision Evaluation Input: Program-level ground truth GTP ∈ {T, NT}; variant-level ground truths (GTVi )1≤i≤n with GTVi ∈ {T, NT}; and variant-level analyzer outputs (OVi )1≤i≤n with OVi ∈ {yes, no, unknown, timeout, error}. Output: A program-level decision d ∈ {correct, wrong} and variant-resolution ratios: (d, ratioT ) if GTP = T, and (d, ratioT , ratioN T ) if GTP = NT. 1 if GTP = T then 2 if ∃ i (1 ≤ i ≤ n). OVi = no then return (wrong, ⊥) ; 3 ratioT ← |{ i | 1 ≤ i ≤ n ∧ OVi = yes }| / n; 4 return (correct, ratioT ); else if ∃ i (1 ≤ i ≤ n). (GTVi = T ∧ OVi = no) ∨ (GTVi = NT ∧ OVi = yes) then return (wrong, ⊥, ⊥) ; 7 ratioT ← |{ i | 1 ≤ i ≤ n ∧ GTVi = T ∧ OVi = yes }| / |{ i | 1 ≤ i ≤ n ∧ GTVi = T }|; 8 ratioN T ← |{ i | 1 ≤ i ≤ n ∧ GTVi = NT ∧ OVi = no }| / |{ i | 1 ≤ i ≤ n ∧ GTVi = NT }|; 9 return (correct, ratioT , ratioN T );

5

6

time-limit exceedance, and error an internal tool failure. This variant-level workflow lets us evaluate preprocessing effects while treating analyzers as black boxes. For each tool and configuration, Algorithm 1 aggregates variant-level outputs into a program-level result using the ground truth of both the original program and generated variants. For terminating programs, the result is marked wrong if any variant is classified as non-terminating; otherwise, performance is measured by the fraction of variants proven terminating, denoted ratioT . For non-terminating programs, the result is marked wrong if any variant-level output contradicts the corresponding variant ground truth; otherwise, performance is measured by the fractions of terminating and non-terminating variants correctly classified, denoted ratioT and ratioN T . Together, these metrics capture program-level correctness and variant-level coverage, enabling principled comparison across tools and preprocessing configurations. E. Semantic Scope and Preservation Guarantees We formalize the semantic scope of the transformations and their composition in terms of preserved termination-relevant behaviors rather than full program equivalence. The loopfocused notation and preservation claims range over syntactic loops and exclude non-termination caused solely by recursive call cycles without infinite iteration of such constructs. Preliminaries: Let P be a program, ℓ ∈ Loops(P ) a syntactic loop, and Σ(P ) the set of well-defined initial states of P . For slicing, let C(ℓ) be the loop-local slicing criterion from Section IV-B. Because slicing may remove context that affects reachability of ℓ or the states reaching it, we consider only states that are well-defined in both P and its slice and from which ℓ is reachable in P : Σ(P, ℓ) ≜ {σ ∈ Σ(P ) ∩ Σ(Slice(P, ℓ)) | ℓ is reachable in P from σ}. We also define a reachability-precedence relation on loops. For loops ℓ′ , ℓ ∈ Loops(P ) and state σ, we write ℓ ′ ⪯P σ ℓ if ℓ′ = ℓ or some execution of P from σ encounters ℓ′ before the first encounter of ℓ. For σ ∈ Σ(P, ℓ), we write P, σ ⇓ℓ if

every well-defined execution from σ performs finitely many iterations of ℓ, and P, σ ⇑ℓ if some such execution performs infinitely many iterations. For concretization, let T be the selected input assignments, each complete and type-correct for the nondeterministic input occurrences in the input specification. For t ∈ T , P [t] denotes the semantic restriction of P where each specified __VERIFIER_nondet_*() outcome is fixed according to t, with repeated evaluations of the same syntactic occurrence fixed consistently to the same value. Thus, P [t] represents one selected input scenario. For σ ∈ Σ(P ), we write P [t], σ ⇓ and P [t], σ ⇑ for termination and divergence under t. For combined slicing and concretization, P [t], σ ⇓ℓ and P [t], σ ⇑ℓ denote finite and infinite iteration of ℓ, respectively, under t. Assumption IV.1 (Loop-criterion adequacy of generated slices). For each generated slice Slice(P, ℓ), we assume that the slicing backend preserves the loop-local criterion C(ℓ), which comprises the guard-relevant reads of ℓ, the annotated loop-control locations inside ℓ, and their data and control dependencies. Thus, executions from states in Σ(P, ℓ) that reach ℓ have corresponding sliced executions with the same retained criterion behavior, and any sliced loop-divergence relevant here arises from behavior retained from P , either infinite iteration of ℓ itself or divergence of a loop that can be encountered before ℓ in P . The preservation results below are conditional loop-focused consequences of this adequacy, not claims of whole-program semantic equivalence. Theorem IV.2 (Loop-focused non-termination preservation under slicing). Under Assumption IV.1, for every program P , loop ℓ ∈ Loops(P ), and state σ ∈ Σ(P, ℓ): 1) P, σ ⇑ℓ =⇒ Slice(P, ℓ), σ ⇑ℓ ; 2) Slice(P, ℓ), σ ⇑ℓ =⇒ ∃ℓ′ ∈ Loops(P ). ℓ′ ⪯P σ ℓ ∧ σ ∈ Σ(P, ℓ′ ) ∧ P, σ ⇑ℓ′ . Proof sketch. For (1), Assumption IV.1 ensures that any execution of P from σ witnessing infinite iteration of ℓ has a corresponding execution in Slice(P, ℓ) with the same retained behavior relevant to C(ℓ). Hence, the slice preserves nontermination of the selected loop obligation. For (2), assume that Slice(P, ℓ) has an infinite execution of ℓ from σ. By

7

Assumption IV.1, this execution is justified by criterion behavior retained from P . If the corresponding original execution reaches ℓ, the divergence is the selected loop divergence itself. Otherwise, the obstruction occurs earlier, in some loop ℓ′ encountered before the first encounter of ℓ from σ. Thus, the sliced divergence is accounted for by an original-program divergence in ℓ or in a loop preceding ℓ from σ. Theorem IV.3 (Loop-focused termination preservation under slicing). Under Assumption IV.1, for every program P , loop ℓ ∈ Loops(P ), and state σ ∈ Σ(P, ℓ): 1) Slice(P, ℓ), σ ⇓ℓ =⇒ P, σ ⇓ℓ ;
′ 2) ∀ℓ′ ∈ Loops(P ). ℓ′ ⪯P σ ℓ∧σ ∈ Σ(P, ℓ ) ⇒ P, σ ⇓ℓ′ =⇒ Slice(P, ℓ), σ ⇓ℓ . Proof sketch. For (1), we argue by contraposition using Theorem IV.2(1). Any infinite iteration of ℓ in P would be preserved as divergence of the corresponding loop-focused obligation in Slice(P, ℓ). Hence, termination of that obligation in the slice implies termination of ℓ in P . For (2), contraposition with Theorem IV.2(2) shows that any infinite loop-focused execution in the slice would be accounted for by divergence of some original-program loop preceding ℓ from σ. Since the premise rules out all such divergences, the selected loopfocused obligation in the slice must terminate. These are loopfocused claims, not whole-program equivalence claims. Theorem IV.4 (Scenario-level correctness of concretization). For every program P , complete and type-correct input assignment t ∈ T , and initial state σ ∈ Σ(P ): 1) P [t], σ ⇑⇐⇒ Cncrt(P, t), σ ⇑; 2) P [t], σ ⇓⇐⇒ Cncrt(P, t), σ ⇓. Proof sketch. The semantic program P [t] is P restricted to the selected input assignment t. The transformation Cncrt(P, t) implements this restriction syntactically by replacing each specified __VERIFIER_nondet_*() occurrence with the corresponding type-correct literal from t, while preserving declarations, expression contexts, control flow, and evaluation order. Because t fixes all specified nondeterministic inputs, including repeated evaluations of the same syntactic occurrence, executions of P [t] and Cncrt(P, t) from the same initial state are step-for-step identical. Thus, under t, the two programs have the same terminating and diverging executions. Corollary IV.5 (Scenario-level loop-focused preservation under slicing and concretization). Under Assumption IV.1, for every program P , loop ℓ ∈ Loops(P ), input assignment t ∈ T , and state σ ∈ Σ(P, ℓ): 1) P [t], σ ⇑ℓ =⇒ Cncrt(Slice(P, ℓ), t), σ ⇑ℓ ; 2) Cncrt(Slice(P, ℓ), t), σ ⇑ℓ =⇒ ∃ℓ′ ∈ Loops(P ). ℓ′ ⪯P σ ℓ∧ σ ∈ Σ(P, ℓ′ ) ∧ P [t], σ ⇑ℓ′ ; 3) Cncrt(Slice(P, ℓ), t), σ ⇓ℓ =⇒ P [t], σ ⇓ℓ ; ′ 4)
∀ℓ′ ∈ Loops(P ). ℓ′ ⪯P σ ℓ ∧ σ ∈ Σ(P, ℓ ) ⇒ P [t], σ ⇓ℓ′ =⇒ Cncrt(Slice(P, ℓ), t), σ ⇓ℓ . Proof sketch. The combined variant Cncrt(Slice(P, ℓ), t) is the loop-focused slice under the fixed input assignment t. By Theorem IV.4, concretization preserves exactly the executions of the selected scenario. By Assumption IV.1, the slice preserves the criterion behavior needed for the selected

loop obligation, with retained nondeterministic occurrences remaining compatible with the concretization mapping. Instantiating Theorems IV.2 and IV.3 within scenario t yields the four claims. Thus, divergence of the selected original loop obligation under t is preserved in the sliced-and-concretized variant, while divergence of the combined variant is reflected, under the same assignment, by divergence of ℓ itself or of a loop that can be encountered before ℓ from σ. The termination claims follow by the same contrapositive reasoning as in Theorem IV.3. Hence, the result is scenario-level and loopfocused, not a whole-program equivalence claim. V. I MPLEMENTATION We implemented F OCUS TNT as a C++23 source-level preprocessing framework for C programs, using Clang LibTooling for source-to-source transformations and Frama-C for slicing, without modifying downstream (non-)termination analyzers. Loop-based slicing uses a Clang front end to identify for, while, and do–while loops, extract loop descriptors, and emit slicing metadata. It annotates loop-control statements (continue, break, goto, and return) to preserve termination-relevant control flow. The slicing backend invokes Frama-C in batch mode, running Evolved Value Analysis (EVA) with the slicing plugin to generate compilable sliced variants. For loops outside main, caller- and callee-context slices are merged through lightweight source transformations to retain relevant interprocedural context. ACSL annotations are removed after slicing for analyzers that do not accept ACSL. Input-driven concretization is a Clang-based specialization pass. Given a tabular input specification, F OCUS TNT replaces each __VERIFIER_nondet_*() occurrence with the corresponding type-correct literal for a selected input assignment while preserving declarations and control structure. It produces one variant per input assignment, can be applied to original or sliced programs, and serves as input-scenario specialization rather than standalone input generation. A top-level driver orchestrates preprocessing and analysis: for each program, it applies the selected configuration, generates variants, and runs the configured analyzers under fixed resource limits. It normalizes outcomes to yes, no, unknown, timeout, and error, records wall-clock runtimes, generates machine-readable logs, and implements Algorithm 1 to aggregate outcomes against program- and variant-level ground truth, producing program-level decisions and ratioT and ratioN T values. VI. E XPERIMENTAL S ETUP This section describes the experimental setup, including benchmarks, tools, configurations, measurements, and research questions. A. Benchmarks We evaluate our approach on the benchmark suite introduced by Shi et al. [18], [30], which contains 117 simplified C/C++ programs derived from real-world OSS nontermination bugs: 56 non-terminating cases and 61 corresponding terminating fixes. The suite was constructed using explicit

8

filtering and simplification criteria and includes program patterns that are challenging for many analyzers, such as pointers, arrays, structured data, bitwise operations, bounded arithmetic, and recursion. Accordingly, some tools in our study do not aim to provide sound (non-)termination guarantees for all benchmark patterns, consistent with observations by Shi et al.1 The benchmark provides program-level ground-truth labels2 for termination and non-termination. Our preprocessing pipeline generates additional variants through slicing and input-driven concretization. For generated variants, we assign labels according to the semantics of the corresponding program instance, enabling consistent aggregation of verification outcomes across variants. For concretization, we generate ten input assignments per program. For non-terminating programs, these assignments cover both terminating and diverging executions when feasible, using five terminating and five non-terminating scenarios where such a split can be established; for terminating programs, all assignments correspond to terminating executions. This controlled construction exposes distinct execution domains while preserving comparability across programs. B. Tools We evaluate six widely studied (non-)termination analyzers: Athena, Proton, UAutomizer, AProVE, CPAchecker, and 2LS. Together, they span diverse verification paradigms, including logic-based fixpoint reasoning, bounded-model-checking witness generation, trace abstraction with interpolation refinement, symbolic-execution-based termination analysis, configurable program analysis, and bounded model checking with kinduction and template-based invariant synthesis. Experiments were conducted on an Apple M2 Pro machine with a 10core CPU and 16 GB RAM, running macOS 15.6.1 and 64bit Linux Docker containers to provide a consistent execution environment. Tool configurations follow prior evaluations on this benchmark, and all tools use a uniform five-minute timeout per analyzed variant. C. Configurations For each program and analyzer, we evaluate four configurations that differ only in the preprocessing applied by F O CUS TNT, with backend analyzers and parameters unchanged: 1) BASE: analysis of the original program 2) S LICE: analysis of loop-based slices 3) C NCRT: analysis of concretized variants 4) S LICE +C NCRT: analysis of variants obtained by applying slicing before concretization These configurations isolate the individual and combined effects of structural isolation and semantic specialization. The reverse order, C NCRT +S LICE, may produce different slices because concretization can change reachability and dependence information. However, we evaluate S LICE +C NCRT to 1 Athena was designed to soundly support the semantic setting of the Shi et al. benchmark suite. 2 We use corrected labels for two mislabeled benchmarks: Incorrect_Initialization_2_T (non-terminating) and Signed_Overflow_Error_1_NT (terminating).

avoid recomputing expensive loop-targeted slices for each input assignment. D. Measurements For each analyzed program variant, we record the analyzer outcome—yes, no, unknown, timeout, or error—and the wallclock time, including preprocessing and backend analysis. Outcomes are aggregated following Algorithm 1, yielding a program-level decision and the variant-resolution ratios ratio T and ratio N T . For runtime, we report three per-program statistics: Total Variant Time (TVT), the cumulative runtime over generated variants; Average Variant Time (AVT), TVT divided by the number of variants; and Median Variant Time (MVT), which reduces sensitivity to outliers. To compare the cost of successful verification, we compute timing statistics over correctly solved programs. We also report the Solved Ratio (SR), the proportion of programs included in the timing analysis. E. Research Questions Our evaluation is guided by the following research questions. • RQ1 (Accuracy Impact). For each verification tool, to what extent do S LICE, C NCRT, and S LICE +C NCRT change the number of correctly classified (non-)terminating programs relative to BASE, and what factors explain these changes? • RQ2 (Complementarity to B ASE ). To what extent do S LICE, C NCRT, and S LICE +C NCRT complement BASE by correctly handling programs for which BASE yields an incorrect or inconclusive outcome? • RQ3 (Loop-Level Localization of (Non-)Termination). To what extent does S LICE localize an inconclusive programlevel outcome to specific loops by producing conclusive (non-)termination results for the remaining loops? • RQ4 (Feature Sensitivity). Which structural and datatype characteristics are associated with successful (non)termination analysis under BASE, S LICE, C NCRT, and S LICE +C NCRT? • RQ5 (Incorrect Classification Reduction). Do S LICE , C N CRT , and S LICE +C NCRT reduce incorrect (non-)termination classifications relative to BASE? • RQ6 (Efficiency and Runtime Impact). Compared to BASE, how do S LICE, C NCRT, and S LICE +C NCRT affect TVT, AVT, and MVT for correctly solved programs, and how should these costs be interpreted with respect to SR? • RQ7 (Tractability–Generality Trade-offs). What tradeoffs arise between detectability, solver tractability, and the semantic scope over which correctness or divergence is established under S LICE, C NCRT, and S LICE +C NCRT? • RQ8 (Integration Potential). Do the empirical effects of S LICE, C NCRT, and S LICE +C NCRT justify their integration into BASE verification, and if so, how should they be incorporated? VII. R ESULTS This section presents the empirical findings organized according to the research questions.

9

(a) Results for non-terminating benchmarks. Correct, ratioT ≥ 0%, ratioN T > 0% denotes program-level non-termination detection, since at least one non-terminating variant is classified as non-terminating. Correct, ratioT ≥ 0%, ratioN T ≥ 50% and Correct, ratioT ≥ 0%, ratioN T = 100% denote the same program-level detection with stronger variant-level coverage, where at least half or all non-terminating variants are classified as non-terminating. W rong denotes a variant-level classification inconsistent with ground truth.

(b) Results for terminating benchmarks. Correct, ratioT = 100% denotes program-level termination resolution, since all generated variants are classified as terminating. Correct, ratioT ≥ 50% and Correct, ratioT > 0% denote partial variant-level resolution, where at least half or at least one generated variant is classified as terminating, but program-level termination remains unresolved. W rong denotes a variant-level classification inconsistent with ground truth.

Fig. 4: Accuracy under preprocessing configurations. Bars report the number of benchmarks satisfying the corresponding outcome criterion for each analyzer and preprocessing configuration. Results for C NCRT and S LICE +C NCRT are evaluated over selected input-scenario variants, not over all nondeterministic executions of the original program.

A. RQ1: Accuracy Impact Figure 4 compares outcome distributions across preprocessing configurations for each analyzer. For correct classifications, we focus on Correct, ratioT ≥ 0%, ratioN T > 0% for non-termination and Correct, ratioT = 100% for termination; the remaining thresholds capture variant-level coverage. The effect of preprocessing is strongly analyzer- and taskdependent: no configuration consistently improves accuracy across all analyzers or both verification tasks. For nontermination under S LICE, Proton (BASE 30 → S LICE 34, +4), CPAchecker (+2), and AProVE (+1) improve, whereas Athena (−4) and UAutomizer (−3) decrease, and 2LS is unchanged. Under C NCRT, 2LS shows the largest gain (BASE 1 → C NCRT 25, +24), followed by AProVE (+6), while the remaining tools decrease by −1 or −2. The task also matters: positive effects are more frequent for non-termination than for termination, with S LICE improving three analyzers on non-termination—

Proton (+4), CPAchecker (+2), and AProVE (+1)—but none on full termination resolution, and S LICE +C NCRT improving four analyzers on non-termination—2LS (+23), AProVE (+6), Proton (+1), and CPAchecker (+1)—whereas only CPAchecker improves on termination (+9). These results suggest that preprocessing benefits depend on interactions among transformed programs, analyzer-specific abstractions and heuristics, and the reasoning demands of termination versus non-termination, so the same transformation may help some analyzers or tasks while having little effect or reducing accuracy for others. Configurations containing C NCRT produce the largest improvements, but only for specific analyzer–task pairs. For nontermination, the largest gains are for 2LS, which increases from 1 under BASE to 25 under C NCRT (+24) and 24 under S LICE +C NCRT (+23), followed by AProVE, which improves from 13 to 19 under both configurations (+6). For termination, CPAchecker has the largest gains, increasing from 10 under

10

BASE to 21 under C NCRT (+11) and 19 under S LICE +C NCRT (+9). Other tools show smaller gains, no change, or marginal decreases. These results suggest that C NCRT can help certain analyzers classify generated instances by reducing nondeterministic variability and specializing analysis to selected inputscenario variants. In contrast, S LICE produces smaller and more mixed changes. For non-termination, changes range from −4 to +4: Proton (BASE 30 → S LICE 34, +4), CPAchecker (20 → 22, +2), and AProVE (13 → 14, +1) improve, while Athena (39 → 35, −4) and UAutomizer (23 → 20, −3) decrease. For termination, S LICE does not increase the number of fully resolved programs for any analyzer; the changes are either small decreases for UAutomizer (−4), AProVE (−3), Athena (−2), and CPAchecker (−1), or no change for Proton and 2LS. Compared with C NCRT-based configurations, S LICE has a smaller effect, suggesting that loop-focused structural isolation can help some analyzers but remains limited because it preserves broader loop-relevant behavior and nondeterminism. Finally, the combination S LICE +C NCRT is not consistently additive. Compared with S LICE, it improves 2 of 6 analyzers on non-termination—2LS (S LICE 1 → S LICE +C NCRT 24, +23) and AProVE (14 → 19, +5)—and 3 of 6 on termination— CPAchecker (+10), Athena (+2), and AProVE (+2). Compared with C NCRT, however, it improves only Proton and CPAchecker on non-termination (+2 each), improves none on termination, and decreases several analyzer–task pairs. Thus, structural isolation and input-scenario specialization are not necessarily additive: depending on analyzer abstractions, heuristics, and reasoning mechanisms, their combination may help or reduce the number of correctly classified programs. RQ1 Takeaway. Preprocessing can improve accuracy, but gains are concentrated in specific analyzer–task pairs rather than being uniform. The largest improvements come from configurations containing C NCRT, while S LICE produces more modest changes and S LICE +C NCRT is not consistently additive.

B. RQ2: Complementarity to the BASE Table I compares preprocessing classifications with the corresponding BASE classifications for each analyzer. The results show that preprocessing complements BASE by solving different benchmark subsets, not simply by adding cases already solved by BASE. For example, on non-termination, S LICE recovers 5 benchmarks for Proton—4 previously unknown and 1 previously wrong—while 1 previously solved benchmark becomes unknown. In contrast, for UAutomizer, S LICE recovers 2 benchmarks but loses 5 previously solved ones. Similarly, on termination, CPAchecker has 13 recoveries under both C NCRT and S LICE +C NCRT, but losses differ: 2 under C NCRT and 4 under S LICE +C NCRT. Thus, preprocessing can both recover and lose cases, changing the benchmark subset handled by each analyzer. This occurs because some transformed cases align better with an analyzer’s abstractions, heuristics, or reasoning mechanisms than the BASE form, while others align less well.

Complementarity also differs by benchmark class and recovery source. For non-termination, the largest recovery rates are U→S under S LICE +C NCRT and C NCRT: 23.4% and 19.8%, respectively. For S LICE +C NCRT, 23.4% corresponds to 45 recoveries out of 192 BASE-unknown non-termination cases: Athena 1, Proton 6, UAutomizer 3, AProVE 9, CPAchecker 3, and 2LS 23. In contrast, the largest W→S recovery rate for non-termination is 13.3%, under both S LICE and S LICE +C NCRT. For termination, the pattern reverses: C NCRT and S LICE +C NCRT recover 54.5% and 45.5% of BASE-wrong cases, compared with 11.0% and 9.8% of BASE-unknown cases. Thus, preprocessing mainly resolves previously inconclusive BASE outcomes for non-termination, but more strongly recovers previously incorrect outcomes for termination. C NCRT provides the strongest complementarity, concentrated in a few analyzer–task pairs, while S LICE yields smaller and more mixed effects. Under C NCRT, the largest recoveries occur for 2LS on non-termination (24: 23 previously unknown and 1 previously wrong), CPAchecker on termination (13), and AProVE on non-termination (8); other recoveries range from 1 to 4. In contrast, S LICE mainly recovers non-termination cases: Proton recovers 5, CPAchecker 4, and UAutomizer and AProVE 2 each, while termination recovery is limited to 1 case for CPAchecker. This reflects the transformations: C N CRT specializes verification to selected input-scenario variants, whereas S LICE simplifies program structure while preserving broader behavior and nondeterminism. Finally, S LICE +C NCRT improves substantially over S LICE, but not consistently over C NCRT. Compared with S LICE, the largest recovery increases are 2LS on non-termination (S LICE 0 → S LICE +C NCRT 23, +23), CPAchecker on termination (+12), and AProVE on non-termination (+7). Compared with C NCRT, gains are smaller: on non-termination, Proton (C NCRT 2 → S LICE +C NCRT 7, +5), CPAchecker (+3), UAutomizer (+1), and AProVE (+1) improve, while 2LS decreases slightly (−1) and Athena is unchanged. On termination, S LICE +C NCRT provides no additional recoveries over C NCRT; results are unchanged or decrease by 1. These results suggest that most complementarity from S LICE +C NCRT comes from concretization: adding slicing helps relative to S LICE alone, but gives little additional benefit once C NCRT has already been applied. RQ2 Takeaway. Preprocessing complements BASE selectively: it solves different benchmark subsets and recovers different types of BASE failures across benchmark classes. The strongest recoveries come from configurations containing C NCRT, while S LICE is more limited and S LICE +C NCRT mainly improves over S LICE, not consistently over C NCRT.

C. RQ3: Loop-Level Localization of (Non-)Termination Table II summarizes loop-level localization under S LICE for benchmarks with different numbers of loops. Although S LICE has limited program-level impact in RQ1 and RQ2, it provides partial loop-level localization for many multi-loop

11

TABLE I: Complementarity to the BASE configuration. Rows denote the classification produced by BASE, and columns denote the classification produced by the applied preprocessing configuration. Each entry reports the number of benchmarks in the corresponding row–column combination for a given analyzer. Transitions from U or W to S indicate recoveries, i.e., benchmarks unresolved or incorrectly classified by BASE but solved after preprocessing, and quantify the complementarity provided by preprocessing. Transitions from S to U or W indicate losses, i.e., benchmarks solved by BASE that become unresolved or incorrectly classified after preprocessing. Results for C NCRT and S LICE +C NCRT are evaluated over selected input-scenario variants, not over all nondeterministic executions of the original program. (a) Results for non-terminating benchmarks. S (Solved) denotes program-level non-termination detection, i.e., at least one non-terminating variant is classified as non-terminating (Correct, ratioT ≥ 0%, ratioN T > 0%). U (Unknown) denotes program-level unresolved cases, i.e., no non-terminating variant is classified as non-terminating (Correct, ratioT ≥ 0%, ratioN T = 0%). W (Wrong) denotes a program-level classification inconsistent with the benchmark ground truth. Applied Configuration S LICE

C NCRT

S LICE +C NCRT

BASE Classification S U W S U W S U W

S 35 0 0 36 1 0 33 1 0

Athena U 4 17 0 3 16 0 6 16 0

W 0 0 0 0 0 0 0 0 0

S 29 4 1 27 2 0 24 6 1

Proton U W 1 0 16 1 1 3 0 3 18 1 0 5 1 5 13 2 3 1

UAutomizer S U W 18 5 0 2 29 0 0 0 2 20 1 2 2 26 3 0 0 2 14 7 2 3 25 3 0 0 2

S 12 2 0 11 8 0 10 9 0

AProVE U W 1 0 36 1 1 3 0 2 27 4 2 2 0 3 26 4 3 1

CPAchecker S U W 18 2 0 3 32 0 1 0 0 18 0 2 1 33 1 0 0 1 17 1 2 3 31 1 1 0 0

S 1 0 0 1 24 0 1 23 0

2LS U 0 51 0 0 28 0 0 28 0

W 0 1 3 0 0 3 0 1 3

(b) Results for terminating benchmarks. S (Solved) denotes program-level termination resolution, i.e., all generated variants are classified as terminating (Correct, ratioT = 100%). U (Unknown) denotes program-level unresolved cases, i.e., fewer than all generated variants are classified as terminating (Correct, ratioT < 100%). W (Wrong) denotes a program-level classification inconsistent with the benchmark ground truth. Applied Configuration S LICE

C NCRT

S LICE +C NCRT

BASE Classification S U W S U W S U W

S 34 0 0 35 4 0 33 3 0

Athena U 2 25 0 1 21 0 3 22 0

W 0 0 0 0 0 0 0 0 0

S 52 0 0 45 1 2 45 1 1

Proton U W 0 0 4 0 1 4 7 0 3 0 0 3 7 0 3 0 1 3

UAutomizer S U W 25 4 0 0 31 0 0 0 1 25 4 0 2 29 0 0 1 0 20 9 0 1 30 0 0 1 0

S 22 0 0 23 2 0 22 2 0

AProVE U W 3 0 36 0 0 0 2 0 34 0 0 0 3 0 34 0 0 0

CPAchecker S U W 8 2 0 1 43 2 0 0 5 8 2 0 9 37 0 4 0 1 6 4 0 9 37 0 4 0 1

S 29 0 0 28 1 0 28 1 0

2LS U 0 32 0 1 31 0 1 31 0

W 0 0 0 0 0 0 0 0 0

TABLE II: Loop-level localization under slicing. The table groups benchmarks by the number of loops n and reports, for each analyzer, how many benchmarks have exactly k resolved loop-specific slices. Resolving k loop-specific slices localizes the original program-level unknown outcome to the remaining n − k unresolved loop-specific slices. In this benchmark set, the maximum number of loops is four. We define partial localization for multi-loop benchmarks as 1 < n ≤ 4 and 0 < k < n, and complete localization as 1 ≤ n ≤ 4 and k = n. (a) Results for non-terminating benchmarks. Loops

Programs

1 2 3 4

37 13 4 2

Athena Resolved Loops 0 1 2 3 4 14 23 – – – 1 5 7 – – 1 1 0 2 – 1 0 1 0 0

Proton Resolved Loops 0 1 2 3 4 13 20 – – – 0 1 12 – – 0 2 1 1 – 1 1 0 0 0

Athena Resolved Loops 0 1 2 3 4 16 25 – – – 5 3 6 – – 1 1 0 2 – 0 1 0 0 1

Proton Resolved Loops 0 1 2 3 4 3 36 – – – 0 0 12 – – 0 0 1 3 – 0 1 0 0 1

UAutomizer Resolved Loops 0 1 2 3 4 25 10 – – – 2 2 9 – – 0 3 1 0 – 1 1 0 0 0

AProVE Resolved Loops 0 1 2 3 4 25 8 – – – 5 4 4 – – 0 3 1 0 – 1 1 0 0 0

CPAchecker Resolved Loops 0 1 2 3 4 21 16 – – – 8 0 5 – – 3 0 1 0 – 2 0 0 0 0

2LS Resolved Loops 0 1 2 3 4 34 0 – – – 10 3 0 – – 1 1 0 1 – 1 1 0 0 0

CPAchecker Resolved Loops 0 1 2 3 4 28 6 – – – 11 0 3 – – 3 0 1 0 – 2 0 0 0 0

2LS Resolved Loops 0 1 2 3 4 20 21 – – – 6 2 6 – – 1 1 1 1 – 0 1 0 0 1

(b) Results for terminating benchmarks. Loops

Programs

1 2 3 4

41 14 4 2

UAutomizer Resolved Loops 0 1 2 3 4 26 14 – – – 2 3 9 – – 0 2 1 1 – 0 1 0 0 1

benchmarks. For non-termination, partial localization is most frequent for AProVE (9 benchmarks), followed by Athena and UAutomizer (7 each). For termination, it is most frequent for UAutomizer (7), followed by AProVE (6) and Athena and

AProVE Resolved Loops 0 1 2 3 4 27 14 – – – 5 2 7 – – 0 2 1 1 – 1 1 0 0 0

2LS (5 each). For example, Athena’s 7 non-termination cases comprise 5 two-loop benchmarks with one resolved slice, 1 three-loop benchmark with one resolved slice, and 1 four-loop benchmark with two resolved slices, localizing the remaining

12

uncertainty to 1, 2, and 2 unresolved loops, respectively. Thus, S LICE can provide diagnostic value even without full programlevel resolution, because resolved slices reduce the set of loops that may be responsible for an unknown outcome. Complete localization becomes less frequent as loop count increases, whereas partial localization remains common in multi-loop benchmarks. For non-termination, complete localization reaches 34.7% for 1-loop and 47.4% for 2-loop benchmarks, but drops to 16.7% for 3-loop and 0% for 4-loop benchmarks. In contrast, partial localization remains visible for larger multi-loop benchmarks: 19.2%, 58.3%, and 41.7% for 2-, 3-, and 4-loop benchmarks, respectively. The 47.4% complete-localization rate for 2-loop benchmarks corresponds to 37 of 13 × 6 analyzer–benchmark pairs in which the whole program, including both loops, is resolved: 7 Athena, 12 Proton, 9 UAutomizer, 4 AProVE, 5 CPAchecker, and 0 2LS. The 58.3% partial-localization rate for 3-loop benchmarks corresponds to 14 of 4 × 6 pairs in which at least one, but not all, loop-specific slices are resolved: 1 Athena, 3 Proton, 4 UAutomizer, 4 AProVE, 1 CPAchecker, and 1 2LS. This difference occurs because complete localization requires resolving all loops, which becomes harder as loop count increases, whereas partial localization only requires resolving a subset of loop-specific slices, each analyzed separately using its loop-relevant context. Finally, partial localization is analyzer- and task-dependent. AProVE has the largest partial-localization count for nontermination (9), UAutomizer has the largest count for termination (7), and CPAchecker has the smallest count in both benchmark classes (1). Moreover, every analyzer has equal or higher partial-localization counts for non-termination than for termination: Athena (7 vs. 5), Proton (5 vs. 2), UAutomizer (7 vs. 7), AProVE (9 vs. 6), CPAchecker (1 vs. 1), and 2LS (5 vs. 5). Thus, the same loop-level decomposition provides different localization benefits across analyzers, and S LICE narrows unresolved non-termination cases at least as often as termination cases. RQ3 Takeaway. S LICE provides diagnostic value through loop-level localization rather than program-level resolution. Complete localization decreases as loop count increases, but partial localization remains common. Both effects are analyzer-dependent and stronger for nontermination than termination.

D. RQ4: Feature Sensitivity Table III reports outcomes for benchmark groups characterized by different structural and data-type features under each preprocessing configuration. The results show that preprocessing is feature-dependent, and that responsive feature categories vary across analyzers and verification tasks. For example, on non-termination, AProVE improves on Pointer Manipulation from 0 solved programs under BASE to 2 under both C N CRT and S LICE +C NCRT, but shows no improvement on Bit Calculation, where all configurations leave 5 programs unknown. Thus, for the same analyzer, preprocessing helps some feature categories but not others. Responsive features also

differ across analyzers: although AProVE does not improve on Bit Calculation, 2LS improves from 0 solved programs under BASE to 5 under both C NCRT and S LICE +C NCRT. The task also matters: although AProVE improves on nontermination Pointer Manipulation, the corresponding termination benchmarks show no improvement, with all configurations solving 1 program and leaving 6 unknown. This suggests that preprocessing helps when transformed tasks match analyzerspecific feature reasoning, but may have little effect on poorly handled features; termination and non-termination reasoning can further change which features benefit. Preprocessing is most effective on Integer Underflow/Overflow and Bit Calculation benchmarks, while Recursion and Data Structure benchmarks respond weakest. On nontermination, Integer Underflow/Overflow shows gains for four analyzers: UAutomizer (+1 under S LICE; BASE 3 → S LICE 4), AProVE (+1, +1, and +2 under S LICE, C NCRT, and S LICE +C NCRT), CPAchecker (+3 and +2 under S LICE and S LICE +C NCRT), and 2LS (+9 under both C NCRT and S LICE +C NCRT). In contrast, Recursion improves only for AProVE (+2 under both C NCRT and S LICE +C NCRT), with no gains for Athena, Proton, CPAchecker, or 2LS. These results suggest that preprocessing is most beneficial when the main challenge involves arithmetic or bit-level behavior that can be simplified or specialized, whereas recursion and complex data structures require reasoning capabilities that preprocessing alone does not substantially provide. Finally, configurations containing C NCRT produce the largest feature-specific improvements, while S LICE alone yields smaller and more mixed effects. The largest gains under C NCRT occur for 2LS on non-termination Integer Underflow/Overflow (BASE 1 → C NCRT 10, +9), CPAchecker on termination Bit Calculation (+8), and CPAchecker on termination Integer Underflow/Overflow (+6). S LICE +C NCRT matches C NCRT on these cases, showing that adding S LICE is not consistently additive. In contrast, S LICE alone ranges from −4 (UAutomizer on non-termination Recursion) to +3 (CPAchecker on non-termination Integer Underflow/Overflow). This suggests that the largest gains are mainly driven by input-scenario specialization: C NCRT exposes specific behaviors without requiring reasoning over all nondeterminism, whereas S LICE mainly removes surrounding context and has smaller, analyzer- and feature-dependent effects. RQ4 Takeaway. Preprocessing effects are strongly feature-sensitive. Arithmetic and bit-level categories benefit most, especially under configurations containing C N CRT , while recursion and data-structure benchmarks show limited gains. The responsive features still vary across analyzers and verification tasks. E. RQ5: Incorrect Classification Reduction Our results show that preprocessing does not consistently reduce incorrect classifications relative to BASE; its effect varies across analyzers, benchmark classes, and configurations. Figure 4 shows that, for termination, incorrect classifications decrease for Proton (BASE 5 → S LICE 4, C NCRT/S LICE +C NCRT

13

TABLE III: Structural sensitivity under preprocessing configurations. Rows group benchmarks by structural or data-type feature, and entries report the number of benchmarks classified as S, U, or W by each analyzer under each configuration. S, U, and W follow the definitions in Table I. Results for C NCRT and S LICE +C NCRT are evaluated over selected input-scenario variants, not over all nondeterministic executions of the original program. (a) Results for non-terminating benchmarks. Features (Total) Pointer Manipulation (7)

Array (8)

Data Structure (3)

Bit Calculation (5) Integer Underflow/ Overflow (14)

Recursion (12)

Configuration BASE S LICE C NCRT S LICE +C NCRT BASE S LICE C NCRT S LICE +C NCRT BASE S LICE C NCRT S LICE +C NCRT BASE S LICE C NCRT S LICE +C NCRT BASE S LICE C NCRT S LICE +C NCRT BASE S LICE C NCRT S LICE +C NCRT

Athena S U 4 3 2 5 2 5 1 6 4 4 3 5 3 5 3 5 2 1 1 2 2 1 1 2 5 0 5 0 5 0 5 0 14 0 13 1 14 0 13 1 0 12 0 12 0 12 0 12

W 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

S 4 5 6 6 3 4 5 4 3 3 3 3 4 5 4 5 9 9 9 9 0 0 0 0

Proton U W 3 0 2 0 1 0 0 1 5 0 4 0 2 1 1 3 0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 1 4 3 2 1 4 5 0 11 1 11 1 11 1 11 1

UAutomizer S U W 2 5 0 2 5 0 2 3 2 2 3 2 2 6 0 2 6 0 2 3 3 1 3 4 2 1 0 2 1 0 2 1 0 2 1 0 2 2 1 2 2 1 2 2 1 2 2 1 3 9 2 4 8 2 2 10 2 3 9 2 4 8 0 0 12 0 4 8 0 0 12 0

S 0 0 2 2 0 1 1 1 0 0 1 1 0 0 0 0 1 2 2 3 2 2 4 4

AProVE U W 7 0 7 0 5 0 5 0 8 0 7 0 6 1 5 2 3 0 3 0 2 0 2 0 5 0 5 0 5 0 5 0 9 4 8 4 9 3 10 1 10 0 10 0 8 0 8 0

CPAchecker S U W 0 7 0 0 7 0 0 7 0 0 7 0 0 8 0 0 8 0 0 8 0 0 8 0 0 3 0 0 3 0 0 3 0 0 3 0 5 0 0 5 0 0 5 0 0 5 0 0 7 6 1 10 4 0 7 5 2 9 4 1 0 12 0 0 12 0 0 12 0 0 12 0

S 0 0 1 1 0 0 2 1 0 0 1 1 0 0 5 5 1 1 10 10 0 0 0 0

2LS U 7 6 6 5 8 7 6 6 3 3 2 2 5 5 0 0 13 13 4 4 9 9 9 9

W 0 1 0 1 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 3 3 3 3

AProVE U W 6 0 6 0 6 0 6 0 5 0 6 0 5 0 5 0 3 0 3 0 3 0 3 0 12 0 12 0 12 0 12 0 14 0 15 0 15 0 16 0 9 0 9 0 9 0 9 0

CPAchecker S U W 0 7 0 0 7 0 0 7 0 0 7 0 0 8 0 0 8 0 0 8 0 0 8 0 0 3 0 0 3 0 0 3 0 0 3 0 1 9 3 1 8 4 9 4 0 9 4 0 4 14 3 4 12 5 10 10 1 10 10 1 0 12 0 0 12 0 0 12 0 0 12 0

S 0 0 0 0 3 3 3 3 0 0 0 0 6 6 6 6 13 13 12 12 4 4 4 4

2LS U 7 7 7 7 5 5 5 5 3 3 3 3 7 7 7 7 8 8 9 9 8 8 8 8

W 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

(b) Results for terminating benchmarks. Features (Total) Pointer Manipulation (7)

Array (8)

Data Structure (3)

Bit Calculation (13) Integer Underflow/ Overflow (21)

Recursion (12)

Configuration BASE S LICE C NCRT S LICE +C NCRT BASE S LICE C NCRT S LICE +C NCRT BASE S LICE C NCRT S LICE +C NCRT BASE S LICE C NCRT S LICE +C NCRT BASE S LICE C NCRT S LICE +C NCRT BASE S LICE C NCRT S LICE +C NCRT

Athena S U 0 7 0 7 1 6 1 6 4 4 3 5 4 4 3 5 0 3 0 3 1 2 1 2 10 3 10 3 10 3 10 3 17 4 16 5 17 4 15 6 0 12 0 12 0 12 0 12

W 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

S 2 2 4 3 5 5 7 6 1 1 1 1 13 13 13 13 20 20 17 17 10 10 9 9

Proton U W 2 3 2 3 2 1 2 2 2 1 2 1 1 0 1 1 0 2 0 2 1 1 1 1 0 0 0 0 0 0 0 0 0 1 1 0 3 1 4 0 2 0 2 0 3 0 3 0

3), UAutomizer (BASE 1 → C NCRT/S LICE +C NCRT 0), and CPAchecker (BASE 5 → C NCRT/S LICE +C NCRT 1), although S LICE increases CPAchecker incorrect classifications from 5 to 7. For non-termination, reductions are limited to S LICE for Proton (5 → 4) and CPAchecker (1 → 0); by contrast, C NCRT and S LICE +C NCRT increase incorrect counts for several analyzers, including Proton (5 → 9/8), UAutomizer (2 → 7/7), AProVE (4 → 8/8), and CPAchecker (1 → 4/3). Table I explains why incorrect counts can both decrease and

UAutomizer S U W 1 6 0 1 6 0 2 5 0 2 5 0 5 3 0 5 3 0 4 4 0 4 4 0 0 3 0 0 3 0 0 3 0 0 3 0 6 6 1 6 6 1 5 7 0 5 8 0 8 12 1 8 12 1 7 13 0 7 14 0 3 9 0 0 12 0 3 9 0 0 12 0

S 1 1 1 1 3 2 3 3 0 0 0 0 1 1 1 1 7 6 6 5 3 3 3 3

increase. For termination, Proton’s 5 BASE-wrong cases are partly removed: S LICE turns one into unknown, C NCRT solves two, and S LICE +C NCRT solves one while turning another into unknown. Thus, preprocessing can reduce incorrect outcomes either by enabling a correct result or by avoiding an incorrect conclusive one. However, it can also create new incorrect outcomes. For CPAchecker with S LICE, the 5 BASE-wrong termination cases remain wrong, while 2 BASE-unknown cases become wrong. This means preprocessing makes additional

14

benchmarks conclusive, but some are classified incorrectly. For Proton with C NCRT on non-termination, the 5 BASEwrong cases remain wrong, and 4 new incorrect cases appear, 3 of which were previously correct under BASE. Thus, even semantics-preserving transformations can change how backend analyzers respond to verification tasks. Incorrect classifications require particular attention. Ideally, semantics-preserving preprocessing should preserve or improve correctness, and analyzer performance should improve or at least not deteriorate, since slicing and concretization are intended to simplify verification of transformed instances. However, our results show that incorrect classifications and performance deterioration remain challenges for several tools. This aligns with prior studies showing that (non-)termination analyzers often perform well on theoretical benchmarks such as TermCOMP and SV-COMP, but struggle more with realworld-driven C programs involving complex features and lowlevel semantics. The observed variation across configurations is informative: transformed benchmarks can expose backend analyzer limitations, and these mixed outcomes provide useful evidence for improving (non-)termination tools. For application programmers, the results indicate when preprocessing should be used cautiously and interpreted as part of a portfolio workflow. For tool developers, they identify analyzer–feature and analyzer–transformation combinations where additional engineering is needed to improve robustness beyond increasing solved counts. Figure 4 further shows that configurations differ in the magnitude and direction of incorrect-classification changes. S LICE produces only small changes, mostly 0 or ±1, with one larger increase for CPAchecker on termination (+2). In contrast, C NCRT has the strongest changes in both directions: it yields the largest reductions for termination, especially CPAchecker (−4) and Proton (−2), but also the largest increases for non-termination, especially UAutomizer (+5), Proton (+4), and AProVE (+4). S LICE +C NCRT largely mirrors C NCRT: it preserves the same termination reductions, especially for CPAchecker (−4) and Proton (−2), and similar non-termination increases, especially for UAutomizer (+5), AProVE (+4), and Proton (+3). This suggests that S LICE is relatively conservative, whereas C NCRT-based configurations have stronger mixed effects: input-scenario specialization can make additional variants conclusive, but not necessarily correctly classified. Finally, Table III shows that feature-level changes in incorrect classifications are concentrated in specific analyzer– feature combinations rather than distributed uniformly across features. Reductions occur mainly in Integer Underflow/Overflow and Bit Calculation. For Integer Underflow/Overflow, incorrect classifications decrease on non-termination for Proton (−2 under S LICE, −4 under S LICE +C NCRT), AProVE (−1 under C NCRT, −3 under S LICE +C NCRT), and CPAchecker (−1 under S LICE), and on termination for Proton under S LICE and S LICE +C NCRT and for UAutomizer and CPAchecker under C NCRT and S LICE +C NCRT. In contrast, increases concentrate mainly in non-termination Array and Pointer Manipulation benchmarks. For Array, incorrect classifications increase under C NCRT/S LICE +C NCRT for Proton, UAutomizer, and

AProVE by +1/+3, +3/+4, and +1/+2, respectively, and under S LICE/S LICE +C NCRT for 2LS by +1/+1. This suggests that preprocessing helps when the remaining task matches an analyzer’s strengths, whereas Array and Pointer Manipulation cases may become conclusive without fully resolving the underlying memory- and aliasing-related difficulty. RQ5 Takeaway. Preprocessing does not consistently reduce incorrect classifications. S LICE has relatively conservative effects, whereas C NCRT-based configurations produce larger but mixed changes, with feature-level effects concentrated in specific analyzer–feature pairs. F. RQ6: Efficiency and Runtime Impact Table IV compares runtime efficiency across preprocessing configurations. Because TVT, AVT, and MVT are computed over correctly solved programs, they should be interpreted together with SR: lower runtime may reflect a smaller or easier solved subset, while higher runtime may reflect additional solved cases or generated variants. Configurations containing C NCRT substantially increase total analysis cost (TVT), whereas S LICE usually has a smaller effect. For example, for Athena on termination, TVT increases from 8.11s under BASE to 32.54s under C NCRT and 57.22s under S LICE +C NCRT, while S LICE changes it only slightly to 8.56s. This is expected because TVT accumulates runtime across all analyzed variants, and C NCRT-based configurations introduce additional input-scenario variants. Despite increasing total runtime, preprocessing can reduce per-variant runtime (AVT), depending on the analyzer and benchmark class. For Athena on termination, AVT decreases from 8.11s under BASE to 5.22s under S LICE, 4.25s under C NCRT, and 4.74s under S LICE +C NCRT. In contrast, Proton’s non-termination AVT increases from 3.37s under BASE to 6.80s under S LICE, 8.88s under C NCRT, and 6.52s under S LICE +C NCRT. Since AVT normalizes by the number of analyzed variants, these results show that preprocessing can make individual variants easier to analyze, but not uniformly across analyzers and benchmark classes. Finally, configurations containing C NCRT generally affect typical-case runtime (MVT) more than S LICE, though the direction depends on the analyzer and benchmark class. For Proton’s termination benchmarks, MVT increases slightly from 43.70s under BASE to 47.24s under S LICE, but drops to 7.43s under C NCRT and 7.82s under S LICE +C NCRT. For CPAchecker’s non-termination benchmarks, MVT remains unchanged under S LICE but increases to 4.86s under both C NCRT and S LICE +C NCRT. Because MVT reflects a typical analyzed variant and is less sensitive to outliers than AVT, C NCRT-based configurations alter typical-variant difficulty more strongly than S LICE, with effects that may be positive or negative. RQ6 Takeaway. Preprocessing increases total analysis cost mainly by generating additional variants, but it does not uniformly make those variants harder to analyze. Pervariant runtime effects vary across analyzers and benchmark classes.

15

TABLE IV: Efficiency and runtime impact under preprocessing configurations. Entries report the average Solved Ratio (SR), average Total Variant Time (TVT), average Average Variant Time (AVT), and median Median Variant Time (MVT) for nonterminating (NT) and terminating (T) benchmarks across analyzers and configurations. Runtime statistics are computed over correctly solved programs. Results for C NCRT and S LICE +C NCRT are evaluated over selected input-scenario variants, not over all nondeterministic executions of the original program. Metric

Avg. SR (%)

Avg. TVT (s)

Avg. AVT (s)

Med. MVT (s)

Configuration BASE S LICE C NCRT S LICE +C NCRT BASE S LICE C NCRT S LICE +C NCRT BASE S LICE C NCRT S LICE +C NCRT BASE S LICE C NCRT S LICE +C NCRT

Athena NT T 69.64 59.02 63.10 59.15 59.64 69.34 57.32 66.04 14.27 8.11 14.19 8.56 29.33 32.54 35.49 57.22 14.27 8.11 10.88 5.22 3.57 4.25 3.54 4.74 1.97 1.87 1.88 1.87 1.72 1.73 1.75 1.77

Proton NT T 53.57 85.25 62.65 88.39 64.11 90.82 67.38 90.77 3.37 76.71 12.07 119.89 63.14 90.72 80.76 129.53 3.37 76.71 6.80 73.04 8.88 10.92 6.52 9.44 2.03 43.70 2.08 47.24 6.07 7.43 5.60 7.82

G. RQ7: Tractability–Generality Trade-offs The results show a trade-off among detectability, solver cost, and semantic scope. Configurations containing C NCRT can improve detectability for selected analyzers, but establish correctness or divergence only over selected input-scenario variants, not all nondeterministic executions. In contrast, S LICE preserves broader loop-relevant behavior and program semantics, but usually yields smaller detectability gains; its main benefit is diagnostic localization of unresolved behavior to specific loops. The tractability cost also differs: S LICE has limited overhead, whereas C NCRT and S LICE +C NCRT can increase TVT by generating additional variants. However, AVT and MVT show that some variants become easier to analyze, so higher TVT does not necessarily imply worse per-variant tractability. RQ7 Takeaway. C NCRT improves detectability by specializing inputs, but narrows semantic scope and can increase total cost. S LICE preserves broader behavior and mainly helps localization, while S LICE +C NCRT combines both effects without consistently dominating either. H. RQ8: Integration Potential In principle, sound preprocessing should improve analyzer results; mixed outcomes suggest limitations in how backend analyzers handle transformed tasks. Our results support integrating S LICE, C NCRT, and S LICE +C NCRT into BASE verification as complementary options rather than replacements. Across RQ1–RQ5, no configuration is uniformly best: each may improve, degrade, or leave results unchanged depending on the analyzer, benchmark class, and program features. RQ2 further shows that preprocessing solves different benchmark subsets from BASE. Thus, S LICE supports structural simplification and loop-level localization, C NCRT supports input-scenario specialization, and S LICE +C NCRT may help when both effects are relevant. The behavior of C NCRT

UAutomizer NT T 41.07 47.54 39.14 46.04 48.93 57.54 43.10 53.25 4.68 3.90 7.35 7.07 23.44 50.42 30.90 64.95 4.68 3.90 4.11 3.38 4.17 9.86 3.19 7.80 0.00 0.00 0.00 2.41 3.00 2.76 2.64 2.73

AProVE NT T 23.21 40.98 28.42 40.30 41.96 53.44 45.60 50.87 2.11 3.68 3.33 5.61 20.58 27.88 32.44 35.54 2.11 3.68 2.71 3.69 4.26 4.29 3.45 2.82 0.00 0.00 0.00 0.00 3.16 2.94 3.23 2.81

CPAchecker NT T 35.71 16.39 38.69 15.85 41.79 46.39 42.53 45.52 2.14 18.71 2.92 1.83 41.97 98.40 43.32 76.95 2.14 18.71 2.28 1.31 5.07 26.34 4.75 7.75 0.00 0.00 0.00 0.00 4.86 4.85 4.86 4.83

2LS NT 1.79 6.70 39.64 42.77 0.01 0.06 1.47 2.09 0.01 0.04 0.24 0.27 0.00 0.00 0.36 0.36

T 47.54 51.23 57.38 61.37 0.20 0.34 2.35 3.67 0.20 0.22 0.29 0.31 0.00 0.29 0.37 0.37

and S LICE +C NCRT also suggests potential for hybrid static– dynamic workflows, with effects depending on the analyzer, task, and program features. Accordingly, integration should be adaptive: retain BASE as the default reference, then selectively apply S LICE for difficult loop structures, C NCRT when nondeterministic input scenarios limit analysis, and S LICE +C NCRT when both effects may help. Results should be interpreted in a portfolio style. RQ8 Takeaway. Preprocessing should be integrated as an adaptive portfolio. BASE should remain the default reference, while S LICE, C NCRT, and S LICE +C NCRT are applied selectively based on the likely source of analysis difficulty. VIII. D ISCUSSION This section discusses and summarizes the main implications of the empirical results. a) Preprocessing as analyzer-, task-, and featuredependent refinement: The empirical results show that preprocessing acts as an analyzer-, task-, and feature-dependent refinement rather than a uniformly beneficial optimization. Across analyzers and verification tasks, preprocessing changes the set of cases each analyzer handles instead of monotonically improving on BASE, with effects generally more visible for non-termination than for full termination resolution. Outcomes also vary across features: arithmetic and bit-level benchmarks benefit most often, whereas recursion and datastructure benchmarks show more limited gains. This variation helps application programmers interpret preprocessing outcomes cautiously and provides tool developers with evidence of analyzer–feature and analyzer–transformation interactions that require stronger support. b) Configuration-level effects and trade-offs: S LICE, C NCRT, and S LICE +C NCRT modify different dimensions of the verification task. S LICE removes termination-irrelevant

16

context and isolates loop-level obligations; C NCRT reduces nondeterministic input variability by analyzing selected inputscenario variants; and S LICE +C NCRT combines structural isolation with input specialization. Their effects differ in magnitude and direction: S LICE is generally the most conservative, improving loop-level localization and producing modest, mixed changes in solved cases and incorrect classifications. C NCRT is more aggressive, yielding the largest gains in some analyzer–task pairs and reducing certain incorrect classifications, but it can also lose solved cases or increase incorrect classifications when specialization changes the behaviors exposed to the analyzer. S LICE +C NCRT can help when both structural coupling and nondeterminism hinder analysis, but its benefits are not consistently additive beyond C NCRT. The configurations also differ in generality and cost: S LICE preserves broader loop-relevant behavior, whereas C NCRT and S LICE +C NCRT narrow semantic scope to selected variants; similarly, S LICE usually has moderate cost, while C NCRTbased configurations may improve per-variant tractability but increase total runtime by generating multiple variants. c) Toward adaptive integration: These results suggest that preprocessing is most useful not as a replacement for BASE, but as a complementary way to obtain alternative views of difficult verification cases. When original analysis is inconclusive, transformed variants can help indicate whether the difficulty is associated with loop structure, input variability, analyzer limitations, or feature-specific reasoning gaps. Overall, the results support an adaptive workflow in which preprocessing complements, diagnoses, and supports originalprogram analysis. IX. T HREATS TO VALIDITY This section discusses the main threats to validity and mitigation steps. a) Construct validity: A main threat concerns how concretized variants represent the original program. Input-driven concretization depends on the input-generation strategy, number of generated inputs, and behavioral diversity of those inputs; different choices may expose different execution domains and affect quantitative results. Since our goal is to study verification behavior under input-scenario specialization, not input generation, concretized variants should be interpreted as selected input-scenario instances: they preserve behavior for exercised inputs but do not establish (non-)termination for all nondeterministic executions of the original program. b) Internal validity: Generated variants and their groundtruth labels require controlled validation to preserve semantic consistency. We mitigate this by assigning labels according to each generated program instance and applying a consistent aggregation policy across configurations. However, validation may limit scalability to larger benchmark sets, and alternative aggregation policies could yield different program-level summaries. In addition, concretization benefits depend on whether backend analyzers exploit fixed input values. Because our pipeline does not add analyzer-specific instrumentation or extra constant-propagation passes, these differences remain part of the measured analyzer behavior.

c) Performance validity: Configurations that generate multiple variants may introduce opportunity bias relative to BASE, since verification effort is distributed across several decomposed analyses rather than one original-program analysis. Efficiency conclusions also depend on the runtime model: TVT captures cumulative runtime across variants, while AVT and MVT capture per-variant and typical-case costs over correctly solved programs. We therefore report TVT, AVT, MVT, and SR together to relate runtime cost to the solved subset used for timing analysis. Conclusions may still vary with timeout budgets, hardware, tool settings, or variant-generation policies. d) External validity: Generality is limited by the selected benchmark suite and analyzers. Although the benchmarks are real-world-driven and include challenging C/C++ features, and the analyzers cover diverse verification paradigms, the observed effects may differ for other suites, larger codebases, semantic models, language features, or (non-)termination tools. X. C ONCLUSION AND F UTURE W ORK We presented F OCUS TNT, a lightweight, tool-independent preprocessing front end for C programs that applies loopbased slicing and input-driven concretization before (non)termination analysis. Our empirical study shows that preprocessing is not uniformly beneficial: its effects depend on the analyzer, verification task, and program features. S LICE provides conservative structural isolation and loop-level localization, whereas C NCRT can improve detectability for selected input-scenario variants at the cost of narrower semantic scope and additional analysis effort. The combined S LICE +C NCRT configuration is not consistently additive. Overall, the results support using preprocessing adaptively as a complement to BASE, providing alternative verification views that help diagnose difficult cases and guide future analyzer engineering. Our findings suggest several directions for future work. First, adaptive preprocessing strategies could decide when and how to apply slicing or concretization, guided by structural features or early analysis feedback. Such strategies could preserve preprocessing benefits while avoiding unnecessary variant generation and analyzer-sensitive regressions. Second, input discovery for concretization could be improved through lightweight search, heuristic exploration, or coverage-guided generation to expose informative behaviors. Third, future work could extend the loop-focused slicing criteria and preservation arguments to recursive call structures. Fourth, the empirical scope could be broadened by evaluating additional analyzers and benchmark suites, including larger real-world codebases with richer C/C++ features. Finally, future work could study whether these source-level transformations extend beyond termination analysis to tasks such as safety verification, liveness reasoning, or resource-bound inference. DATA AVAILABILITY The artifacts supporting this paper are publicly available at https://github.com/negarfathi/FocusTNT, including the implementation, benchmarks, evaluation results, and reproduction scripts.

17

ACKNOWLEDGMENTS The authors used OpenAI ChatGPT (GPT-4o) [53] solely for grammar checking, language editing, and clarity improvement. All of these edits were reviewed and validated by the authors, who take full responsibility for the final manuscript. R EFERENCES [1] B. Cook, A. Podelski, and A. Rybalchenko, “Termination proofs for systems code,” in Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation, ser. PLDI ’06. New York, NY, USA: Association for Computing Machinery, 2006, p. 415–426. [Online]. Available: https://doi.org/10.1145/1133981.1134029 [2] X. Xie, B. Chen, L. Zou, S.-W. Lin, Y. Liu, and X. Li, “Loopster: static loop termination analysis,” in Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ser. ESEC/FSE 2017. New York, NY, USA: Association for Computing Machinery, 2017, p. 84–94. [Online]. Available: https://doi.org/10.1145/3106237.3106260 [3] H.-Y. Chen, B. Cook, C. Fuhs, K. Nimkar, and P. O’Hearn, “Proving nontermination via safety,” in Tools and Algorithms for the Construction and Analysis of Systems, E. Ábrahám and K. Havelund, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2014, pp. 156–171. [4] D. Larraz, K. Nimkar, A. Oliveras, E. Rodrı́guez-Carbonell, and A. Rubio, “Proving non-termination using max-smt,” in Computer Aided Verification, A. Biere and R. Bloem, Eds. Cham: Springer International Publishing, 2014, pp. 779–796. [5] C. Urban, “The abstract domain of segmented ranking functions,” in Static Analysis, F. Logozzo and M. Fähndrich, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 43–62. [6] A. Bakhirkin, J. Berdine, and N. Piterman, “A forward analysis for recurrent sets,” in Static Analysis, S. Blazy and T. Jensen, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2015, pp. 293–311. [7] M. Colón and H. Sipma, “Practical methods for proving program termination,” in Proceedings of the 14th International Conference on Computer Aided Verification, ser. CAV ’02. Berlin, Heidelberg: Springer-Verlag, 2002, p. 442–454. [8] A. R. Bradley, Z. Manna, and H. B. Sipma, “Linear ranking with reachability,” in Proceedings of the 17th International Conference on Computer Aided Verification, ser. CAV’05. Berlin, Heidelberg: Springer-Verlag, 2005, p. 491–504. [Online]. Available: https://doi.org/ 10.1007/11513988 48 [9] D. Kroening, N. Sharygina, A. Tsitovich, and C. M. Wintersteiger, “Termination analysis with compositional transition invariants,” in Proceedings of the 22nd International Conference on Computer Aided Verification, ser. CAV’10. Berlin, Heidelberg: SpringerVerlag, 2010, p. 89–103. [Online]. Available: https://doi.org/10.1007/ 978-3-642-14295-6 9 [10] M. Colón and H. Sipma, “Synthesis of linear ranking functions,” in Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, ser. TACAS 2001. Berlin, Heidelberg: Springer-Verlag, 2001, p. 67–81. [11] A. Podelski and A. Rybalchenko, “A complete method for the synthesis of linear ranking functions,” in Verification, Model Checking, and Abstract Interpretation, B. Steffen and G. Levi, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2004, pp. 239–251. [12] J. Leike and M. Heizmann, “Ranking templates for linear loops,” in Tools and Algorithms for the Construction and Analysis of Systems, E. Ábrahám and K. Havelund, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2014, pp. 172–186. [13] A. M. Ben-Amram and S. Genaim, “Ranking functions for linearconstraint loops,” J. ACM, vol. 61, no. 4, Jul. 2014. [Online]. Available: https://doi.org/10.1145/2629488 [14] A. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, and R.-G. Xu, “Proving non-termination,” in Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ser. POPL ’08. New York, NY, USA: Association for Computing Machinery, 2008, p. 147–158. [Online]. Available: https://doi.org/10.1145/1328438.1328459 [15] B. Cook, C. Fuhs, K. Nimkar, and P. O’Hearn, “Disproving termination with overapproximation,” in Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, ser. FMCAD ’14. Austin, Texas: FMCAD Inc, 2014, p. 67–74. [16] TermCOMP Contributors, “TermCOMP/TPDB: The termination problems data base,” https://github.com/TermCOMP/TPDB, 2024, accessed: July 6, 2026. [Online]. Available: https://github.com/TermCOMP/TPDB

[17] SV-Benchmarks Contributors, “SV-Benchmarks: Benchmark suite for software verification,” https://github.com/sosy-lab/sv-benchmarks/, 2025, accessed: July 6, 2026. [Online]. Available: https://github.com/ sosy-lab/sv-benchmarks/ [18] X. Shi, X. Xie, Y. Li, Y. Zhang, S. Chen, and X. Li, “Large-scale analysis of non-termination bugs in real-world oss projects,” in Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ser. ESEC/FSE 2022. New York, NY, USA: Association for Computing Machinery, 2022, p. 256–268. [Online]. Available: https: //doi.org/10.1145/3540250.3549129 [19] B. Cook, A. Podelski, and A. Rybalchenko, “Proving program termination,” Commun. ACM, vol. 54, no. 5, pp. 88–98, May 2011. [Online]. Available: https://doi.org/10.1145/1941487.1941509 [20] T. C. Le, T. Antonopoulos, P. Fathololumi, E. Koskinen, and T. Nguyen, “Dynamite: dynamic termination and non-termination proofs,” Proc. ACM Program. Lang., vol. 4, no. OOPSLA, Nov. 2020. [Online]. Available: https://doi.org/10.1145/3428257 [21] H. Karmarkar, R. K. Medicherla, R. Metta, and P. Yeduru, “Fuzznt : Checking for program non-termination,” in 2022 IEEE International Conference on Software Maintenance and Evolution (ICSME), 2022, pp. 409–413. [22] Y. Zhang, X. Xie, Y. Li, S. Chen, C. Zhang, and X. Li, “Endwatch: A practical method for detecting non-termination in real-world software,” in Proceedings of the 38th IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’23. IEEE Press, 2024, p. 686–697. [Online]. Available: https://doi.org/10.1109/ASE56229.2023. 00061 [23] N. Fathi, H. Unno, T. Terauchi, and R. Purandare, “Sound termination and non-termination analysis of c programs with bit-precise bounded semantics and advanced constructs,” Proc. ACM Softw. Eng., vol. 3, no. FSE, Jul. 2026. [Online]. Available: https://doi.org/10.1145/3808205 [24] R. Metta, H. Karmarkar, K. Madhukar, R. Venkatesh, and S. Chakraborty, “Proton: Probes for termination or not (competition contribution),” in Tools and Algorithms for the Construction and Analysis of Systems, B. Finkbeiner and L. Kovács, Eds. Cham: Springer Nature Switzerland, 2024, pp. 393–398. [25] D. Mukhopadhyay, R. Metta, H. Karmarkar, and K. Madhukar, “Proton 2.1: Synthesizing ranking functions via fine-tuned locally hosted llm (competition contribution),” in Tools and Algorithms for the Construction and Analysis of Systems, A. Gurfinkel and M. Heule, Eds. Cham: Springer Nature Switzerland, 2025, pp. 242–247. [26] M. Heizmann, J. Hoenicke, and A. Podelski, “Termination analysis by learning terminating programs,” in Computer Aided Verification, A. Biere and R. Bloem, Eds. Cham: Springer International Publishing, 2014, pp. 797–813. [27] J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann, “Proving termination of programs automatically with aprove,” in Automated Reasoning, S. Demri, D. Kapur, and C. Weidenbach, Eds. Cham: Springer International Publishing, 2014, pp. 184–191. [28] D. Beyer and M. E. Keremoglu, “Cpachecker: a tool for configurable software verification,” in Proceedings of the 23rd International Conference on Computer Aided Verification, ser. CAV’11. Berlin, Heidelberg: Springer-Verlag, 2011, p. 184–190. [29] P. Schrammel and D. Kroening, “2ls for program analysis,” in Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9636. Berlin, Heidelberg: Springer-Verlag, 2016, p. 905–907. [Online]. Available: https://doi.org/10.1007/978-3-662-49674-9 56 [30] FSE2022benchmarks, “FSE-2022-Termination (v1.0),” https://github. com/FSE2022benchmarks/-FSE-2022-Termination/tree/v1.0, 2022, accessed: July 6, 2026. [Online]. Available: https://github.com/ FSE2022benchmarks/-FSE-2022-Termination/tree/v1.0 [31] M. Weiser, “Program slicing,” in Proceedings of the 5th International Conference on Software Engineering, ser. ICSE ’81. IEEE Press, 1981, p. 439–449. [32] B. Korel and J. Laski, “Dynamic program slicing,” Information Processing Letters, vol. 29, no. 3, pp. 155–163, 1988. [Online]. Available: https://www.sciencedirect.com/science/article/pii/0020019088900543 [33] P. Anderson and M. Zarins, “The codesurfer software understanding platform,” in 13th International Workshop on Program Comprehension (IWPC’05), 2005, pp. 147–148. [34] P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, “Frama-c: a software analysis perspective,” in Proceedings of the 10th International Conference on Software Engineering and Formal Methods, ser. SEFM’12. Berlin, Heidelberg:

18

Springer-Verlag, 2012, p. 233–247. [Online]. Available: https://doi.org/ 10.1007/978-3-642-33826-7 16 [35] M. Chalupa, “Dg: Analysis and slicing of llvm bitcode,” in Automated Technology for Verification and Analysis: 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19–23, 2020, Proceedings. Berlin, Heidelberg: Springer-Verlag, 2020, p. 557–563. [Online]. Available: https://doi.org/10.1007/978-3-030-59152-6 33 [36] S. K. Sahoo, J. Criswell, C. Geigle, and V. Adve, “Using likely invariants for automated software fault localization,” in Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems, ser. ASPLOS ’13. New York, NY, USA: Association for Computing Machinery, 2013, p. 139–152. [Online]. Available: https://doi.org/10.1145/2451116.2451131 [37] H. Unno, T. Terauchi, and E. Koskinen, “Constraint-based relational verification,” in Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I. Berlin, Heidelberg: Springer-Verlag, 2021, p. 742–766. [Online]. Available: https://doi.org/10.1007/978-3-030-81685-8 35 [38] S. Kura, H. Unno, and I. Hasuo, “Decision tree learning in cegisbased termination analysis,” in Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part II. Berlin, Heidelberg: Springer-Verlag, 2021, p. 75–98. [Online]. Available: https://doi.org/10.1007/978-3-030-81688-9 4 [39] H. Unno, T. Terauchi, Y. Gu, and E. Koskinen, “Modular primaldual fixpoint logic solving for temporal verification,” Proc. ACM Program. Lang., vol. 7, no. POPL, Jan. 2023. [Online]. Available: https://doi.org/10.1145/3571265 [40] M. Heizmann, J. Christ, D. Dietsch, E. Ermis, J. Hoenicke, M. Lindenmann, A. Nutz, C. Schilling, and A. Podelski, “Ultimate automizer with smtinterpol,” in Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, ser. TACAS’13. Berlin, Heidelberg: SpringerVerlag, 2013, p. 641–643. [Online]. Available: https://doi.org/10.1007/ 978-3-642-36742-7 53 [41] M. Heizmann, D. Dietsch, J. Leike, B. Musa, and A. Podelski, “Ultimate automizer with array interpolation,” in Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9035. Berlin, Heidelberg: Springer-Verlag, 2015, p. 455–457. [Online]. Available: https://doi.org/10.1007/978-3-662-46681-0 43 [42] M. Heizmann, D. Dietsch, M. Greitschus, J. Leike, B. Musa, C. Schätzle, and A. Podelski, “Ultimate automizer with two-track proofs,” in Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9636. Berlin, Heidelberg: Springer-Verlag, 2016, p. 950–953. [Online]. Available: https://doi.org/10.1007/978-3-662-49674-9 68 [43] M. Heizmann, Y.-F. Chen, D. Dietsch, M. Greitschus, J. Hoenicke, Y. Li, A. Nutz, B. Musa, C. Schilling, T. Schindler, and A. Podelski, “Ultimate automizer and the search for perfect interpolants,” in Tools and Algorithms for the Construction and Analysis of Systems, D. Beyer and M. Huisman, Eds. Cham: Springer International Publishing, 2018, pp. 447–451. [44] J. Hensel, F. Emrich, F. Frohn, T. Ströder, and J. Giesl, “Aprove: Proving and disproving termination of memory-manipulating c programs,” in Tools and Algorithms for the Construction and Analysis of Systems, A. Legay and T. Margaria, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2017, pp. 350–354. [45] J. Hensel, J. Giesl, F. Frohn, and T. Ströder, “Proving termination of programs with bitvector arithmetic by symbolic execution,” in Software Engineering and Formal Methods, R. De Nicola and E. Kühn, Eds. Cham: Springer International Publishing, 2016, pp. 234–252. [46] T. Ströder, C. Aschermann, F. Frohn, J. Hensel, and J. Giesl, “Aprove: Termination and memory safety of c programs,” in Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9035. Berlin, Heidelberg: Springer-Verlag, 2015, p. 417–419. [Online]. Available: https://doi.org/10.1007/978-3-662-46681-0 32 [47] V. Malı́k, Š. Martiček, P. Schrammel, M. Srivas, T. Vojnar, and J. Wahlang, “2ls: Memory safety and non-termination,” in Tools and Algorithms for the Construction and Analysis of Systems, D. Beyer and M. Huisman, Eds. Cham: Springer International Publishing, 2018, pp. 417–421. [48] H.-Y. Chen, C. David, D. Kroening, P. Schrammel, and B. Wachter, “Bit-precise procedure-modular termination analysis,” vol. 40, no. 1. New York, NY, USA: Association for Computing Machinery, Dec. 2017. [Online]. Available: https://doi.org/10.1145/3121136

[49] ——, “Synthesising interprocedural bit-precise termination proofs,” in Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’15. IEEE Press, 2015, p. 53–64. [Online]. Available: https://doi.org/10.1109/ASE.2015.10 [50] The LLVM Project, “The LLVM compiler infrastructure project,” https://llvm.org, 2019, accessed: July 6, 2026. [Online]. Available: https://llvm.org [51] C. Cadar, D. Dunbar, and D. Engler, “Klee: unassisted and automatic generation of high-coverage tests for complex systems programs,” in Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, ser. OSDI’08. USA: USENIX Association, 2008, p. 209–224. [52] M. Zalewski, “American fuzzy lop (afl),” https://lcamtuf.coredump. cx/afl/, 2015, accessed: July 6, 2026. [Online]. Available: https: //lcamtuf.coredump.cx/afl/ [53] OpenAI, “ChatGPT (GPT-4o),” https://openai.com/index/hello-gpt-4o/, 2024, accessed: July 6, 2026. [Online]. Available: https://openai.com/ index/hello-gpt-4o/