Loop-Based Slicing and Input-Driven Concretization: An Empirical Study of Termination and Non-Termination Analysis
- URL: http://arxiv.org/abs/2607.08988v1
- Date: Thu, 09 Jul 2026 23:29:19 GMT
- Title: Loop-Based Slicing and Input-Driven Concretization: An Empirical Study of Termination and Non-Termination Analysis
- Abstract summary: This paper presents an empirical study of lightweight, tool-independent source-level preprocessing for (non-)termination analysis.<n>We implement FocusTNT, a C front end that applies loop-based slicing to isolate loop-level obligations and input-driven concretization.<n>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.
- Score: 1.84316002191515
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- 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 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.
Related papers
- CauSec: Unboxing the Causal Drivers of Static Vulnerability Analysis Performance [51.50254897627053]
Static Application Security Testing (SAST) tools are widely used in both industry and academia.<n>These tools often make design choices that sacrifice detection to achieve higher performance.<n>This paper seeks to address this question by relying on a key observation that the assumptions made by these tools are generally of a causal nature.
arXiv Detail & Related papers (2026-08-19T12:56:00Z) - From Prediction to Collaboration: Interactive Symbolic Music Analysis [8.180530393436326]
We present a unified framework for symbolic Roman-numeralRN analysis.<n>It combines strong predictive performance with direct support for constrained completion and revision.<n>It supports complete score analysis, targeted revision of existing labels, and inference of missing annotations from partial context.
arXiv Detail & Related papers (2026-07-15T08:28:43Z) - Finite-Sample Analysis of Nonlinear Independent Component Analysis:Sample Complexity and Identifiability Bounds [1.624454100511275]
Independent Component Analysis (ICA) is a fundamental unsupervised learning technique foruncovering structure in data by separating mixed signals into their independent sources.<n>The finite-sample statistical properties of learning algorithms remain poorly understood.<n>This paper presents a comprehensive finite-sample analysis of nonlinear ICA with neural network encoders.
arXiv Detail & Related papers (2026-04-10T01:15:27Z) - Dynamic analysis enhances issue resolution [53.50448142467294]
DAIRA (Dynamic Analysis-enhanced Issue Resolution Agent) is an automated repair framework that embeds dynamic analysis into the agent's reasoning cycle.<n> Driven by a Test Tracing-Driven methodology, DAIRA utilizes lightweight monitors to extract critical runtime data.<n>When powered by Gemini 3 Flash Preview, DAIRA establishes a new state-of-the-art (SOTA) performance, achieving a 79.4% resolution rate on the SWE-bench Verified dataset.
arXiv Detail & Related papers (2026-03-23T14:48:54Z) - Act, Think or Abstain: Complexity-Aware Adaptive Inference for Vision-Language-Action Models [7.802379200026965]
We propose an adaptive framework that dynamically routes VLA execution based on the complexity of the perceived state.<n>Our approach transforms the VLA's vision-language backbone into an active detection tool by projecting latent embeddings into an ensemble of parametric and non-parametric estimators.
arXiv Detail & Related papers (2026-03-05T13:14:41Z) - Not All Preferences Are Created Equal: Stability-Aware and Gradient-Efficient Alignment for Reasoning Models [52.48582333951919]
We propose a dynamic framework designed to enhance alignment reliability by maximizing the Signal-to-Noise Ratio of policy updates.<n>SAGE (Stability-Aware Gradient Efficiency) integrates a coarse-grained curriculum mechanism that refreshes candidate pools based on model competence.<n> Experiments on multiple mathematical reasoning benchmarks demonstrate that SAGE significantly accelerates convergence and outperforms static baselines.
arXiv Detail & Related papers (2026-02-01T12:56:10Z) - Learning to Align Multi-Faceted Evaluation: A Unified and Robust Framework [61.38174427966444]
Large Language Models (LLMs) are being used more and more extensively for automated evaluation in various scenarios.<n>Previous studies have attempted to fine-tune open-source LLMs to replicate the evaluation explanations and judgments of powerful proprietary models.<n>We propose a novel evaluation framework, ARJudge, that adaptively formulates evaluation criteria and synthesizes both text-based and code-driven analyses.
arXiv Detail & Related papers (2025-02-26T06:31:45Z) - Checkification: A Practical Approach for Testing Static Analysis Truths [0.0]
We propose a method for testing abstract interpretation-based static analyzers.<n>The main advantage of our approach lies in its simplicity, which stems directly from framing it within the Ciao assertion-based validation framework.<n>We have applied our approach to the CiaoPP static analyzer, resulting in the identification of many bugs with reasonable overhead.
arXiv Detail & Related papers (2025-01-21T12:38:04Z) - Smoothness Analysis for Probabilistic Programs with Application to
Optimised Variational Inference [13.836565669337057]
We present a static analysis for discovering differentiable or more generally smooth parts of a given probabilistic program.
We show how the analysis can be used to improve the pathwise gradient estimator.
arXiv Detail & Related papers (2022-08-22T18:18:32Z) - Estimating Structural Target Functions using Machine Learning and
Influence Functions [103.47897241856603]
We propose a new framework for statistical machine learning of target functions arising as identifiable functionals from statistical models.
This framework is problem- and model-agnostic and can be used to estimate a broad variety of target parameters of interest in applied statistics.
We put particular focus on so-called coarsening at random/doubly robust problems with partially unobserved information.
arXiv Detail & Related papers (2020-08-14T16:48:29Z) - Causal Feature Selection for Algorithmic Fairness [61.767399505764736]
We consider fairness in the integration component of data management.
We propose an approach to identify a sub-collection of features that ensure the fairness of the dataset.
arXiv Detail & Related papers (2020-06-10T20:20:10Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.