Pith. sign in

REVIEW 2 major objections 6 minor 54 references

Source-level preprocessing helps termination analyzers only sometimes, and never uniformly: slicing localizes loops, while input concretization trades generality for detectability.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-13 01:11 UTC pith:VX2QXD3U

load-bearing objection Solid multi-tool empirical map of when slicing and concretization help or hurt (non-)termination analysis; the non-uniformity claim is well supported and the soft spots are minor. the 2 major comments →

arxiv 2607.08988 v1 pith:VX2QXD3U submitted 2026-07-09 cs.SE

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

Negar Fathi , Rahul Purandare , Tachio Terauchi , Hiroshi Unno This is my paper
classification cs.SE
keywords termination analysisnon-termination analysisprogram slicinginput concretizationprogram preprocessingempirical evaluationC programsloop isolation
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Proving that a C program always stops, or that it can loop forever, is hard when loops interact and inputs are nondeterministic. This paper does not invent a new prover. It asks whether two simple source rewrites, applied before any existing tool runs, can make the job easier. Loop-based slicing isolates one loop at a time while trying to keep that loop’s termination behavior. Input-driven concretization freezes nondeterministic inputs into a few concrete scenarios. The authors build FocusTNT, feed the original, sliced, concretized, and combined variants to six off-the-shelf analyzers, and measure correctness, complementarity, localization, feature sensitivity, runtime, and semantic scope on 117 real-world-derived programs. The central finding is that the rewrites are not a free win: gains and losses depend on which analyzer, whether the task is termination or non-termination, and which program features are present. Slicing is conservative and mainly localizes hard cases to particular loops; concretization can raise detectability for selected inputs but narrows what is being proved and can raise total cost. Combining the two is not consistently better than either alone. The practical moral is to treat preprocessing as an adaptive complement to analyzing the original program, not as a default replacement.

Core claim

On 117 real-world-derived C/C++ programs and six analyzers, lightweight source-level preprocessing for (non-)termination is not uniformly beneficial. Its impact depends on the analyzer, the termination versus non-termination task, and program features. Loop-based slicing supplies conservative structural isolation and loop-level localization; input-driven concretization can improve detectability for selected input scenarios but narrows semantic scope and may increase analysis effort; their combination is not consistently additive. The results therefore support adaptive use of preprocessing as a complement to original-program analysis.

What carries the argument

FocusTNT’s four configurations—BASE, SLICE, CNCRT, and SLICE+CNCRT—together with Algorithm 1, which aggregates variant-level yes/no/unknown outcomes into a program-level correct/wrong decision and the coverage ratios ratio_T and ratio_NT under explicit ground truth for both the original program and each generated variant.

Load-bearing premise

The slicing backend is assumed to keep exactly the guard reads, control points, and their dependences for each chosen loop, so that a loop’s termination or non-termination in the slice correctly reflects the original program; if a dependence is dropped or over-approximated, the program-level verdict can be wrong.

What would settle it

Re-run the same six analyzers on the same 117 programs after replacing the Frama-C slicing backend with an independent dependence-preserving slicer (or after manually auditing every slice for dropped dependences); if the pattern of gains, losses, and incorrect classifications relative to BASE changes substantially, the loop-criterion adequacy claim and the aggregation results fail.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 6 minor

Summary. This paper presents an empirical study of lightweight, tool-independent source-level preprocessing for termination and non-termination analysis of C programs. The authors implement FocusTNT, which applies loop-based slicing (to isolate loop-level obligations) and input-driven concretization (to specialize nondeterministic inputs into selected scenario variants), alone and in combination. They evaluate four configurations (BASE, SLICE, CNCRT, SLICE+CNCRT) across six analyzers (Athena, Proton, UAutomizer, AProVE, CPAchecker, 2LS) on 117 C/C++ programs derived from real-world non-termination bugs and fixes. The study reports effects on correctness, complementarity to original-program analysis, loop-level localization, feature sensitivity, runtime, semantic scope, and integration potential. The central finding is that preprocessing is not uniformly beneficial: impact depends on analyzer, task, and program features; slicing is conservative and mainly aids localization; concretization can improve detectability for selected scenarios but narrows semantic scope and may raise total cost; and the combination is not consistently additive. The authors therefore recommend adaptive, portfolio-style use of preprocessing as a complement to BASE analysis.

Significance. If the reported non-uniformity result holds—as the multi-tool tables and complementary metrics strongly suggest—the paper makes a useful contribution to software verification practice and tool engineering. Rather than proposing yet another prover, it systematically measures how two natural source-level transformations reshape existing black-box analyzers on real-world-derived C programs. Strengths include: (i) a transparent four-configuration design with six diverse analyzers and corrected ground truth; (ii) explicit semantic-scope theorems (IV.2–IV.5) under a stated assumption, plus Algorithm 1 for principled aggregation; (iii) honest negative and mixed findings (non-additivity, increased incorrect classifications under CNCRT for some tools, feature-dependent effects); and (iv) public artifacts. The practical guidance for application developers interpreting outcomes and for tool developers targeting robustness gaps is a genuine value-add beyond raw solved counts.

major comments (2)
  1. [§VII-A RQ1 / Fig. 4] RQ1 and Fig. 4 frame CNCRT/SLICE+CNCRT outcome counts as “accuracy impact” relative to BASE, but these configurations are intentional under-approximations over selected input scenarios (often including known diverging assignments for NT programs). The large gains (e.g., 2LS NT: BASE 1 → CNCRT 25) therefore measure scenario-level detectability, not comparable whole-program accuracy. The paper caveats this in RQ7, §IV-C, and figure captions, but RQ1’s wording and the side-by-side bars still invite over-reading. Please reframe RQ1 (and the corresponding takeaway) so that BASE accuracy and CNCRT scenario-detectability are not presented as the same metric; keep the numbers, but make the semantic-scope distinction load-bearing in the primary accuracy section, not only later.
  2. [§IV-E Assumption IV.1 / Theorems IV.2–IV.3; RQ3] The loop-focused preservation theorems (IV.2–IV.3, Cor. IV.5) rest on Assumption IV.1 (Frama-C preserves guard-relevant reads, annotated control locations, and their dependences). The abstract and introduction claim that slicing “preserves the analyzed loop’s termination behavior,” and RQ3 interprets resolved slices as localization of the original unknown. The empirical correctness counts remain valid even if the assumption fails (variants have independent ground truth), but the interpretive claims about “conservative structural isolation” and diagnostic localization do not. Either provide a lightweight empirical check of slice adequacy on a sample of the suite, or more carefully separate observational results (analyzer outcomes on generated artifacts) from preservation-based interpretations throughout the abstract, intro, and RQ3.
minor comments (6)
  1. [§VII-D RQ4 / Table III] Table III feature groups are very small for some categories (Data Structure n=3; Bit Calculation NT n=5). The claim that recursion and data-structure benchmarks “respond weakest” should note limited statistical power and avoid over-generalizing from single-digit counts.
  2. [§VI-C Configurations] Only SLICE+CNCRT is evaluated, not CNCRT+SLICE. The text notes that reverse order may change dependence information; a short discussion of why the reverse was omitted (cost) and what bias that might introduce would help readers.
  3. [§IV-C Input-Driven Concretization] Input assignments are LLM-proposed then manually curated (ten per program). This is acknowledged, but a brief characterization of how often candidates were discarded or how terminating vs. diverging splits were chosen would improve reproducibility of the CNCRT setup.
  4. [§IV-D Algorithm 1] Algorithm 1: for terminating programs, any variant classified no yields wrong. Under SLICE, if a multi-loop program has one diverging loop and others terminating, the original GT is NT—so this path is for T programs only. A one-sentence clarification that variant GT is assigned per generated instance (not inherited blindly from the original) would reduce reader confusion.
  5. [Throughout / §II] Minor presentation: “FOCUSTNT” vs “FocusTNT” capitalization is inconsistent between abstract and body; unify. Also “Misusing_Variable_Type_1_NT” and similar identifiers are fine in figures but dense in prose—consider short aliases after first use.
  6. [§III Related Work] Related work on slicing (CodeSurfer, DG, Giri) is adequate; a sentence on how loop-criterion slicing differs from standard backward slicing w.r.t. a single variable would help readers less familiar with verification-oriented slicing.

Circularity Check

0 steps flagged

No significant circularity: pure empirical measurement against independent ground truth and black-box analyzers.

full rationale

The paper's central claims are empirical non-uniformity results (preprocessing helps/hurts depending on analyzer, task, and features; combination not additive; use adaptively as complement to BASE). These rest on running six external analyzers on generated variants and comparing outcomes to program- and variant-level ground-truth labels via Algorithm 1 (Fig. 4, Tables I–IV). No equation, fit, or uniqueness theorem reduces a claimed improvement to an author-constructed input. The loop-focused preservation theorems (IV.2–IV.3, Cor. IV.5) are explicitly conditional on Assumption IV.1 (Frama-C criterion adequacy) and serve only to justify interpreting slices as localization aids; the reported accuracy/complementarity/runtime numbers treat variants as independent instances with their own labels and remain valid observations even if the assumption fails on some programs. Input tables are acknowledged under-approximations (selected scenarios, LLM-proposed then manually curated). Self-citations (Athena [23] by overlapping authors; Shi et al. benchmark) are ordinary tool/benchmark usage, not load-bearing premises that force the non-uniformity claim. The derivation chain is therefore self-contained measurement, not circular.

Axiom & Free-Parameter Ledger

2 free parameters · 3 axioms · 1 invented entities

The central empirical claim rests on a small set of domain assumptions about the slicing backend, the completeness of the curated input tables, and the aggregation policy; no free parameters are fitted to produce the headline non-uniformity result, and the only invented entity is the FocusTNT front-end itself.

free parameters (2)
  • number of input assignments per program = 10
    Fixed at ten (five terminating / five non-terminating when feasible) by the authors; different cardinalities or diversity criteria would change the CNCRT and SLICE+CNCRT outcome counts.
  • per-variant timeout = 5 min
    Uniform five-minute wall-clock limit; longer or shorter budgets alter the unknown/timeout fractions and therefore the complementarity tables.
axioms (3)
  • domain assumption Assumption IV.1: Frama-C preserves the loop-local criterion C(ℓ) (guard reads, annotated control locations, and their data/control dependencies) so that loop-focused termination and non-termination transfer between original and slice.
    Load-bearing for Theorems IV.2–IV.3 and Corollary IV.5; if the backend drops a dependence, program-level aggregation becomes unsound.
  • domain assumption The ten curated input assignments per program are feasible and cover both terminating and diverging scenarios when claimed.
    Inputs are LLM-proposed then manually validated; any systematic bias in the selected scenarios directly affects CNCRT detectability numbers.
  • ad hoc to paper Algorithm 1 aggregation correctly lifts variant-level yes/no/unknown results to a program-level correct/wrong decision given the supplied ground-truth labels.
    The policy (any contradictory variant makes the program wrong; otherwise report ratios) is a design choice of the paper, not a standard theorem.
invented entities (1)
  • FocusTNT preprocessing front-end independent evidence
    purpose: Implements the two source-level transforms and the four analysis configurations without modifying backend analyzers.
    The entity is the authors’ own tool; independent evidence is the public artifact repository, but the transforms themselves are the object of study rather than a new physical or mathematical object.

pith-pipeline@v1.1.0-grok45 · 34031 in / 2703 out tokens · 34919 ms · 2026-07-13T01:11:46.555926+00:00 · methodology

0 comments
read the original 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.

Figures

Figures reproduced from arXiv: 2607.08988 by Hiroshi Unno, Negar Fathi, Rahul Purandare, Tachio Terauchi.

Figure 1
Figure 1. Figure 1: Motivating example for loop-based slicing: [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Motivating example for input-driven concretization: [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Overview of the FOCUSTNT 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 non￾termination. EndWatch [22] targets real-world software by instrumenting loops with state-revisit non-termination oracles and exploring executions via fuzzing and symbol… view at source ↗
Figure 4
Figure 4. Figure 4: Accuracy under preprocessing configurations. Bars report the number of benchmarks satisfying the corresponding [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

54 extracted references · 6 canonical work pages

  1. [1]

    Termination proofs for systems code,

    B. Cook, A. Podelski, and A. Rybalchenko, “Termination proofs for systems code,” inProceedings 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

    doi:10.1145/1133981.1134029 2006

  2. [2]

    Loopster: static loop termination analysis,

    X. Xie, B. Chen, L. Zou, S.-W. Lin, Y . Liu, and X. Li, “Loopster: static loop termination analysis,” inProceedings 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

    doi:10.1145/3106237.3106260 2017

  3. [3]

    Proving nontermination via safety,

    H.-Y . Chen, B. Cook, C. Fuhs, K. Nimkar, and P. O’Hearn, “Proving nontermination via safety,” inTools and Algorithms for the Construction and Analysis of Systems, E. ´Abrah´am and K. Havelund, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2014, pp. 156–171

    2014

  4. [4]

    Proving non-termination using max-smt,

    D. Larraz, K. Nimkar, A. Oliveras, E. Rodr ´ıguez-Carbonell, and A. Ru- bio, “Proving non-termination using max-smt,” inComputer Aided Verification, A. Biere and R. Bloem, Eds. Cham: Springer International Publishing, 2014, pp. 779–796

    2014

  5. [5]

    The abstract domain of segmented ranking functions,

    C. Urban, “The abstract domain of segmented ranking functions,” in Static Analysis, F. Logozzo and M. F ¨ahndrich, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 43–62

    2013

  6. [6]

    A forward analysis for recurrent sets,

    A. Bakhirkin, J. Berdine, and N. Piterman, “A forward analysis for recurrent sets,” inStatic Analysis, S. Blazy and T. Jensen, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2015, pp. 293–311

    2015

  7. [7]

    Practical methods for proving program termination,

    M. Col ´on and H. Sipma, “Practical methods for proving program termination,” inProceedings of the 14th International Conference on Computer Aided Verification, ser. CA V ’02. Berlin, Heidelberg: Springer-Verlag, 2002, p. 442–454

    2002

  8. [8]

    Linear ranking with reachability,

    A. R. Bradley, Z. Manna, and H. B. Sipma, “Linear ranking with reachability,” inProceedings of the 17th International Conference on Computer Aided Verification, ser. CA V’05. Berlin, Heidelberg: Springer-Verlag, 2005, p. 491–504. [Online]. Available: https://doi.org/ 10.1007/11513988 48

    doi:10.1007/11513988 2005

  9. [9]

    Termination analysis with compositional transition invariants,

    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. CA V’10. Berlin, Heidelberg: Springer- Verlag, 2010, p. 89–103. [Online]. Available: https://doi.org/10.1007/ 978-3-642-14295-6 9

    2010

  10. [10]

    Synthesis of linear ranking functions,

    M. Col ´on and H. Sipma, “Synthesis of linear ranking functions,” inPro- ceedings 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

    2001

  11. [11]

    A complete method for the synthesis of linear ranking functions,

    A. Podelski and A. Rybalchenko, “A complete method for the synthesis of linear ranking functions,” inVerification, Model Checking, and Abstract Interpretation, B. Steffen and G. Levi, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2004, pp. 239–251

    2004

  12. [12]

    Ranking templates for linear loops,

    J. Leike and M. Heizmann, “Ranking templates for linear loops,” in Tools and Algorithms for the Construction and Analysis of Systems, E. ´Abrah´am and K. Havelund, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2014, pp. 172–186

    2014

  13. [13]

    Ranking functions for linear- constraint loops,

    A. M. Ben-Amram and S. Genaim, “Ranking functions for linear- constraint loops,”J. ACM, vol. 61, no. 4, Jul. 2014. [Online]. Available: https://doi.org/10.1145/2629488

    work page doi:10.1145/2629488 2014

  14. [14]

    Proving non-termination,

    A. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, and R.-G. Xu, “Proving non-termination,” inProceedings 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

    doi:10.1145/1328438.1328459 2008

  15. [15]

    Disproving termination with overapproximation,

    B. Cook, C. Fuhs, K. Nimkar, and P. O’Hearn, “Disproving termination with overapproximation,” inProceedings of the 14th Conference on Formal Methods in Computer-Aided Design, ser. FMCAD ’14. Austin, Texas: FMCAD Inc, 2014, p. 67–74

    2014

  16. [16]

    TermCOMP/TPDB: The termination prob- lems data base,

    TermCOMP Contributors, “TermCOMP/TPDB: The termination prob- lems data base,” https://github.com/TermCOMP/TPDB, 2024, accessed: July 6, 2026. [Online]. Available: https://github.com/TermCOMP/TPDB

    2024

  17. [17]

    SV-Benchmarks: Benchmark suite for software verification,

    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/

    2025

  18. [18]

    Large-scale analysis of non-termination bugs in real-world oss projects,

    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,” inProceedings 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–26...

    doi:10.1145/3540250.3549129 2022

  19. [19]

    Proving program termination,

    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

    doi:10.1145/1941487.1941509 2011

  20. [20]

    Dynamite: dynamic termination and non-termination proofs,

    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

    work page doi:10.1145/3428257 2020

  21. [21]

    Fuzznt : Checking for program non-termination,

    H. Karmarkar, R. K. Medicherla, R. Metta, and P. Yeduru, “Fuzznt : Checking for program non-termination,” in2022 IEEE International Conference on Software Maintenance and Evolution (ICSME), 2022, pp. 409–413

    2022

  22. [22]

    Endwatch: A practical method for detecting non-termination in real-world software,

    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,” inProceedings 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

    doi:10.1109/ase56229.2023 2024

  23. [23]

    Sound termination and non-termination analysis of c programs with bit-precise bounded semantics and advanced constructs,

    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

    work page doi:10.1145/3808205 2026

  24. [24]

    Proton: Probes for termination or not (competition contribution),

    R. Metta, H. Karmarkar, K. Madhukar, R. Venkatesh, and S. Chakraborty, “Proton: Probes for termination or not (competition contribution),” inTools and Algorithms for the Construction and Analysis of Systems, B. Finkbeiner and L. Kov ´acs, Eds. Cham: Springer Nature Switzerland, 2024, pp. 393–398

    2024

  25. [25]

    Proton 2.1: Synthesizing ranking functions via fine-tuned locally hosted llm (competition contribution),

    D. Mukhopadhyay, R. Metta, H. Karmarkar, and K. Madhukar, “Proton 2.1: Synthesizing ranking functions via fine-tuned locally hosted llm (competition contribution),” inTools and Algorithms for the Construc- tion and Analysis of Systems, A. Gurfinkel and M. Heule, Eds. Cham: Springer Nature Switzerland, 2025, pp. 242–247

    2025

  26. [26]

    Termination analysis by learning terminating programs,

    M. Heizmann, J. Hoenicke, and A. Podelski, “Termination analysis by learning terminating programs,” inComputer Aided Verification, A. Biere and R. Bloem, Eds. Cham: Springer International Publishing, 2014, pp. 797–813

    2014

  27. [27]

    Proving termination of programs automatically with aprove,

    J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Pl ¨ucker, P. Schneider-Kamp, T. Str ¨oder, S. Swiderski, and R. Thie- mann, “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

    2014

  28. [28]

    Cpachecker: a tool for configurable software verification,

    D. Beyer and M. E. Keremoglu, “Cpachecker: a tool for configurable software verification,” inProceedings of the 23rd International Confer- ence on Computer Aided Verification, ser. CA V’11. Berlin, Heidelberg: Springer-Verlag, 2011, p. 184–190

    2011

  29. [29]

    2ls for program analysis,

    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

  30. [31]

    FSE-2022-Termination (v1.0),

    FSE2022benchmarks, “FSE-2022-Termination (v1.0),” https://github. com/FSE2022benchmarks/-FSE-2022-Termination/tree/v1.0, 2022, ac- cessed: July 6, 2026. [Online]. Available: https://github.com/ FSE2022benchmarks/-FSE-2022-Termination/tree/v1.0

    2022

  31. [32]

    Program slicing,

    M. Weiser, “Program slicing,” inProceedings of the 5th International Conference on Software Engineering, ser. ICSE ’81. IEEE Press, 1981, p. 439–449

    1981

  32. [33]

    Dynamic program slicing,

    B. Korel and J. Laski, “Dynamic program slicing,”Information Pro- cessing Letters, vol. 29, no. 3, pp. 155–163, 1988. [Online]. Available: https://www.sciencedirect.com/science/article/pii/0020019088900543

    arXiv 1988

  33. [34]

    The codesurfer software understanding platform,

    P. Anderson and M. Zarins, “The codesurfer software understanding platform,” in13th International Workshop on Program Comprehension (IWPC’05), 2005, pp. 147–148

    2005

  34. [35]

    Frama-c: a software analysis perspective,

    P. Cuoq, F. Kirchner, N. Kosmatov, V . Prevosto, J. Signoles, and B. Yakobowski, “Frama-c: a software analysis perspective,” inProceedings 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

    doi:10.1007/978-3-642-33826-7 2012

  35. [36]

    Dg: Analysis and slicing of llvm bitcode,

    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

    doi:10.1007/978-3-030-59152-6 2020

  36. [37]

    Using likely invariants for automated software fault localization,

    S. K. Sahoo, J. Criswell, C. Geigle, and V . Adve, “Using likely invariants for automated software fault localization,” inProceedings 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]. Avai...

    work page doi:10.1145/2451116.2451131 2013

  37. [38]

    Constraint-based relational verification,

    H. Unno, T. Terauchi, and E. Koskinen, “Constraint-based relational verification,” inComputer 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

    doi:10.1007/978-3-030-81685-8 2021

  38. [39]

    Decision tree learning in cegis- based termination analysis,

    S. Kura, H. Unno, and I. Hasuo, “Decision tree learning in cegis- based termination analysis,” inComputer 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

    doi:10.1007/978-3-030-81688-9 2021

  39. [40]

    Modular primal- dual fixpoint logic solving for temporal verification,

    H. Unno, T. Terauchi, Y . Gu, and E. Koskinen, “Modular primal- dual fixpoint logic solving for temporal verification,”Proc. ACM Program. Lang., vol. 7, no. POPL, Jan. 2023. [Online]. Available: https://doi.org/10.1145/3571265

    doi:10.1145/3571265 2023

  40. [41]

    Ultimate automizer with smtinterpol,

    M. Heizmann, J. Christ, D. Dietsch, E. Ermis, J. Hoenicke, M. Lindenmann, A. Nutz, C. Schilling, and A. Podelski, “Ultimate automizer with smtinterpol,” inProceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, ser. TACAS’13. Berlin, Heidelberg: Springer- Verlag, 2013, p. 641–643. [Online]. Av...

    2013

  41. [43]

    Ultimate automizer with two-track proofs,

    M. Heizmann, D. Dietsch, M. Greitschus, J. Leike, B. Musa, C. Sch ¨atzle, and A. Podelski, “Ultimate automizer with two-track proofs,” inProceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume

  42. [44]

    Berlin, Heidelberg: Springer-Verlag, 2016, p. 950–953. [Online]. Available: https://doi.org/10.1007/978-3-662-49674-9 68

    doi:10.1007/978-3-662-49674-9 2016

  43. [45]

    Ultimate automizer and the search for perfect interpolants,

    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,” inTools and Algorithms for the Construction and Analysis of Systems, D. Beyer and M. Huisman, Eds. Cham: Springer International Publishing, 2018, pp. 447–451

    2018

  44. [46]

    Aprove: Proving and disproving termination of memory-manipulating c programs,

    J. Hensel, F. Emrich, F. Frohn, T. Str ¨oder, 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

    2017

  45. [47]

    Proving termination of programs with bitvector arithmetic by symbolic execution,

    J. Hensel, J. Giesl, F. Frohn, and T. Str ¨oder, “Proving termination of programs with bitvector arithmetic by symbolic execution,” inSoftware Engineering and Formal Methods, R. De Nicola and E. K ¨uhn, Eds. Cham: Springer International Publishing, 2016, pp. 234–252

    2016

  46. [48]

    Aprove: Termination and memory safety of c programs,

    T. Str ¨oder, C. Aschermann, F. Frohn, J. Hensel, and J. Giesl, “Aprove: Termination and memory safety of c programs,” inProceedings 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...

    doi:10.1007/978-3-662-46681-0 2015

  47. [49]

    2ls: Memory safety and non-termination,

    V . Mal ´ık, ˇS. Marti ˇcek, P. Schrammel, M. Srivas, T. V ojnar, and J. Wahlang, “2ls: Memory safety and non-termination,” inTools and Algorithms for the Construction and Analysis of Systems, D. Beyer and M. Huisman, Eds. Cham: Springer International Publishing, 2018, pp. 417–421

    2018

  48. [50]

    Bit-precise procedure-modular termination analysis,

    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

  49. [51]

    Available: https://doi.org/10.1145/3121136

    [Online]. Available: https://doi.org/10.1145/3121136

    work page doi:10.1145/3121136

  50. [52]

    Synthesising interprocedural bit-precise termination proofs,

    ——, “Synthesising interprocedural bit-precise termination proofs,” inProceedings 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

    work page doi:10.1109/ase.2015.10 2015

  51. [53]

    The LLVM compiler infrastructure project,

    The LLVM Project, “The LLVM compiler infrastructure project,” https://llvm.org, 2019, accessed: July 6, 2026. [Online]. Available: https://llvm.org

    2019

  52. [54]

    Klee: unassisted and automatic generation of high-coverage tests for complex systems programs,

    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

    2008

  53. [55]

    American fuzzy lop (afl),

    M. Zalewski, “American fuzzy lop (afl),” https://lcamtuf.coredump. cx/afl/, 2015, accessed: July 6, 2026. [Online]. Available: https: //lcamtuf.coredump.cx/afl/

    2015

  54. [56]

    ChatGPT (GPT-4o),

    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/

    2024