Study finds preprocessing strategies for program termination analysis yield mixed results across analyzers

Determining whether a program will eventually halt or continue running indefinitely is a core problem in software verification, yet current analysis tools struggle with the complexity of real-world C code. A new empirical study examines two source-level preprocessing strategies designed to make this task more tractable.

The Challenge#

Loop interactions and nondeterministic inputs—variables that can take on unpredictable values—are major obstacles for existing verification tools. When programs contain multiple interconnected loops or depend on inputs that could vary widely, determining termination becomes significantly harder. The researchers sought to understand whether lightweight preprocessing could reduce this difficulty without fundamentally changing how analyzers operate.

Preprocessing Strategies Tested#

The study introduces FocusTNT, a C front end that applies two complementary techniques:

• Loop-based slicing: Isolates loop-level obligations to focus analysis on one loop at a time, providing structural simplification and better localization of verification problems.
• Input-driven concretization: Replaces nondeterministic inputs with concrete values from selected scenarios, allowing the analyzer to reason about specific cases rather than all possibilities.

Evaluation Methodology#

Researchers evaluated both techniques and their combination across six different analyzers on 117 C/C++ programs derived from actual non-termination bugs found in real software and their fixes. The assessment measured analyzer correctness, how well preprocessing complemented analysis of the original program, quality of loop-level diagnostics, sensitivity to program features, runtime performance, semantic scope, and potential for integration into existing workflows.

Key Findings#

The results reveal that preprocessing does not uniformly help all tools and programs. Slicing offers conservative structural isolation and improved diagnostics at the loop level, while concretization can make certain bugs easier to detect when using particular input values—but it narrows the semantic scope and may increase the time analyzers need to complete their work. Combining both techniques did not consistently produce additive improvements.