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

Jul 16, 2026

Termination and non-termination are core correctness properties, yet verifying them in real-world C code is hindered by complex loop interactions and environment-driven nondeterministic inputs. The paper provides an empirical evaluation of lightweight, tool-independent source-level preprocessing for (non-)termination analysis. It introduces FOCUSTNT, combining loop-based slicing and input-driven concretization, and tests six configurations across 117 C/C++ programs and six analyzers, analyzing correctness, diagnostics, sensitivity, runtime, semantic scope, and integration guidance.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages18

Reading Time45 min

Introduction

Empirical Evaluation Setup

Preprocessing Approach (FOCUSTNT)

Analyzer Configurations and Datasets

Evaluation Dimensions and Metrics

Loop-Based Slicing and Input-Driven Concretization: An Empirical Study of Termination and Non-Termination Analysis Negar Fathi, Rahul Purandare, Tachio Terauchi, and Hiroshi Unno arXiv :2607 .08988v 1 [ cs . SE] 9 Jul 2026 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 presentsan empirical study of lightweight, tool-independent source-level preprocessing for (non-)termination analysis. We implement FOCUSTNT, 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. INTRODUCTION 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: [nfathi2@huskers.unl.edu](nfathi2@huskers.unl.edu), [rahul@unl.edu](rahul@unl.edu). T. Terauchi is with Waseda University, Tokyo, Japan. Email: ter[auchi@waseda.jp](auchi@waseda.jp). H. Unno is with Tohoku University, Sendai, Japan. Email: hi[roshi.unno@acm.org](roshi.unno@acm.org). 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 behaviorsand generate witnesses when divergence depends on particular input patterns [20], [21], [22] . Ho

FAQs

What preprocessing techniques does the paper evaluate for (non-)termination analysis?

It evaluates loop-based slicing to isolate loop-relevant obligations and input-driven concretization to specialize nondeterministic inputs into selected input-scenario variants, both individually and combined.

How is the evaluation conducted in the study?

The study uses FOCUSTNT and compares four configurations—BASE, SLICE, CNCRT, and SLICE+CNCRT—across six analyzers on 117 C/C++ programs derived from real-world non-termination bugs and their fixes.

What overall conclusions does the paper draw about the usefulness of preprocessing?

Preprocessing is not uniformly beneficial; its impact depends on the analyzer, task, and program features. Slicing provides conservative structural isolation, concretization can improve detectability for selected scenarios but narrows semantic scope, and combining them is not consistently additive.

Jul 16, 2026

Upload by River Wang