pith. sign in

arxiv: 2606.28542 · v1 · pith:HZKVPZMEnew · submitted 2026-06-26 · 💻 cs.LO · cs.PL

KoAT: Automatic Complexity and Termination Analysis of Integer Programs

Nils Lommen , \'El\'eanore Meyer , J\"urgen Giesl This is my paper

Pith reviewed 2026-06-30 01:07 UTC · model grok-4.3

classification 💻 cs.LO cs.PL
keywords integer programscomplexity boundstermination analysismodular inferenceruntime boundssize boundsautomatic verificationprogram analysis
0
0 comments X

The pith

KoAT automatically infers upper runtime and size bounds for parts of integer programs to prove termination and complexity.

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

The paper presents KoAT as a tool for analyzing possibly recursive integer programs to derive complexity bounds and termination proofs. It establishes that an alternating modular inference process, which applies a portfolio of techniques to subprograms, can combine local results into overall bounds. A sympathetic reader would care because this reduces reliance on manual analysis for verifying program behavior. The method breaks the full program into manageable pieces rather than treating it as a single unit. Experimental evaluation supports that the combination often succeeds where isolated techniques might not.

Core claim

KoAT implements an alternating modular inference of upper runtime and size bounds for program parts using a portfolio of different techniques to analyze subprograms, thereby enabling automatic complexity bound inference and termination proofs for possibly recursive integer programs.

What carries the argument

Alternating modular inference of runtime and size bounds, which decomposes programs into subprograms and aggregates results from a portfolio of analysis techniques.

If this is right

  • Termination proofs become available automatically for recursive integer programs.
  • Upper bounds on runtime complexity follow directly from the inferred size and runtime results.
  • The modular breakdown allows analysis of programs too large for non-decomposed methods.
  • Using multiple techniques on subprograms covers cases where any single technique would fail.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same modular structure could be tested on programs with additional features such as arrays or pointers if the subprogram analyzers are extended.
  • Results from KoAT could feed into larger verification pipelines that combine complexity information with safety properties.
  • Expanding the portfolio over time would likely increase the fraction of programs for which bounds are found without changing the overall inference architecture.

Load-bearing premise

The portfolio of techniques succeeds often enough on subprograms for their modular combination to produce useful overall bounds and termination proofs.

What would settle it

A collection of terminating integer programs on which KoAT returns no finite runtime bound or termination proof despite the programs having finite execution.

Figures

Figures reproduced from arXiv: 2606.28542 by \'El\'eanore Meyer, J\"urgen Giesl, Nils Lommen.

Figure 1
Figure 1. Figure 1: Program with two Nested Loops Example 1. Consider the program in [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: An Integer Program Corresponding to [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: KoAT: Automatic Complexity and Termination Analysis of Integer Pro￾grams consecutive loops, we start with the first loop and propagate knowledge about the resulting values of variables to subsequent loops. By handling one subpro￾gram after the other, in the end we obtain a bound on the runtime complexity of the whole program. The approach uses size bounds to infer runtime bounds, i.e., size bounds on the e… view at source ↗
Figure 4
Figure 4. Figure 4: Original Loop while 0 < x ∧ y < z do y ← y + x while 0 < x ∧ y ≥ z do x ← x − 1 [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗
read the original abstract

KoAT is a tool to automatically infer complexity bounds and prove termination of (possibly recursive) integer programs. To this end, KoAT implements an alternating modular inference of upper runtime and size bounds for program parts. In particular, KoAT uses a portfolio of different techniques to analyze subprograms. The power of our approach is demonstrated by an extensive experimental evaluation.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper presents KoAT, a tool for automatically inferring complexity bounds and proving termination of possibly recursive integer programs. It implements an alternating modular inference of upper runtime and size bounds for program parts, using a portfolio of different techniques to analyze subprograms, with the approach's power demonstrated through an extensive experimental evaluation.

Significance. If the experimental claims hold and the modular portfolio combination is effective, the work would provide a practical advance in automated analysis of integer programs by integrating multiple techniques in an alternating fashion, potentially improving bound inference and termination proofs over monolithic approaches.

major comments (1)
  1. [Abstract] Abstract: The central claim that the power of the approach is demonstrated by extensive experimental evaluation is unsupported because the abstract (and provided description) gives no details on benchmarks used, evaluation methodology, how inference steps are justified, or quantitative results; this is load-bearing for assessing whether the portfolio produces useful overall bounds.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the detailed feedback. We address the major comment below and will incorporate revisions to strengthen the manuscript.

read point-by-point responses

  1. Referee: [Abstract] Abstract: The central claim that the power of the approach is demonstrated by extensive experimental evaluation is unsupported because the abstract (and provided description) gives no details on benchmarks used, evaluation methodology, how inference steps are justified, or quantitative results; this is load-bearing for assessing whether the portfolio produces useful overall bounds.

    Authors: We agree that the abstract would benefit from a concise summary of the experimental evaluation to better support the claim. In the revised version, we will expand the abstract to include: (i) the primary benchmark suites used (e.g., the Termination Problems Data Base for integer programs and additional recursive program collections), (ii) a brief description of the evaluation methodology (comparison against state-of-the-art tools via alternating modular bound inference), and (iii) key quantitative results (e.g., the fraction of benchmarks for which runtime/size bounds were successfully inferred or termination proved). This will provide readers with immediate evidence of the portfolio's effectiveness while keeping the abstract within length limits; full details and justification of inference steps remain in the dedicated evaluation section. revision: yes

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper presents KoAT as a tool implementing alternating modular inference of runtime and size bounds for integer programs via a portfolio of analysis techniques on subprograms, with power shown via experimental evaluation. No load-bearing derivation, equation, or prediction is present that reduces by construction to its own inputs, fitted parameters, or self-citation chains. The description is self-contained as an engineering and empirical contribution without mathematical self-definition or renaming of results.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The paper is a description of a software tool rather than a mathematical derivation. No free parameters, axioms, or invented entities are apparent from the abstract.

pith-pipeline@v0.9.1-grok · 5580 in / 1018 out tokens · 33535 ms · 2026-06-30T01:07:14.154821+00:00 · methodology

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

53 extracted references · 40 canonical work pages

  1. [1]

    Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis

    E. Albert, P. Arenas, S. Genaim, and G. Puebla. “Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis”. In:Proc. SAS ’08. LNCS 5079. 2008, pp. 221–237.doi: 10.1007/978-3-540-69166- 2 15

    work page doi:10.1007/978-3-540-69166- 2008

  2. [2]

    Cost Analysis of Object-Oriented Bytecode Programs

    E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. “Cost Analysis of Object-Oriented Bytecode Programs”. In:Theoretical Com- puter Science413.1 (2012), pp. 142–159.doi: 10.1016/j.tcs.2011.07.009

    work page doi:10.1016/j.tcs.2011.07.009 2012

  3. [3]

    On the Inference of Resource Us- age Upper and Lower Bounds

    E. Albert, S. Genaim, and A. N. Masud. “On the Inference of Resource Us- age Upper and Lower Bounds”. In:ACM Transactions on Computational Logic14.3 (2013).doi: 10.1145/2499937.2499943

    work page doi:10.1145/2499937.2499943 2013

  4. [4]

    Re- source Analysis Driven by (Conditional) Termination Proofs

    E. Albert, M. Bofill, C. Borralleras, E. Mart´ ın-Mart´ ın, and A. Rubio. “Re- source Analysis Driven by (Conditional) Termination Proofs”. In:The- ory and Practice of Logic Programming19.5-6 (2019), pp. 722–739.doi: 10.1017/S1471068419000152

    work page doi:10.1017/s1471068419000152 2019

  5. [5]

    Ranking Functions for Linear-Con- straint Loops

    A. M. Ben-Amram and S. Genaim. “Ranking Functions for Linear-Con- straint Loops”. In:Journal of the ACM61.4 (2014), 26:1–26:55.doi: 10. 1145/2629488

    2014

  6. [6]

    On Multiphase-Linear Ranking Func- tions

    A. M. Ben-Amram and S. Genaim. “On Multiphase-Linear Ranking Func- tions”. In:Proc. CAV ’17. LNCS 10427. 2017, pp. 601–620.doi: 10.1007/ 978-3-319-63390-9 32

    2017

  7. [7]

    Multiphase-Linear Ranking Functions and Their Relation to Recurrent Sets

    A. M. Ben-Amram, J. J. Dom´ enech, and S. Genaim. “Multiphase-Linear Ranking Functions and Their Relation to Recurrent Sets”. In:Proc. SAS ’19. LNCS 11822. 2019, pp. 459–480.doi: 10.1007/978-3-030-32304- 2 22

    work page doi:10.1007/978-3-030-32304- 2019

  8. [9]

    Golem: A Flexible and Efficient Solver for Constrained Horn Clauses

    M. Blicha, K. Britikov, and N. Sharygina. “Golem: A Flexible and Efficient Solver for Constrained Horn Clauses”. In:Formal Methods in System De- sign67 (2025), pp. 143–160.doi: 10.1007/s10703-025-00470-9

    work page doi:10.1007/s10703-025-00470-9 2025

  9. [10]

    A Modular Static Cost Analysis for GPU Warp-Level Parallelism

    G. Blike, H. Zicarelli, U. Sathiyamoorthy, J. Lange, and T. Cogumbreiro. “A Modular Static Cost Analysis for GPU Warp-Level Parallelism”. In: Proceedings of the ACM on Programming Languages10.POPL (2026), pp. 1471–1499.doi: 10.1145/3776693

    work page doi:10.1145/3776693 2026

  10. [11]

    Proving Termination Through Conditional Ter- mination

    C. Borralleras, M. Brockschmidt, D. Larraz, A. Oliveras, E. Rodr´ ıguez- Carbonell, and A. Rubio. “Proving Termination Through Conditional Ter- mination”. In:Proc. TACAS ’17. LNCS 10205. 2017, pp. 99–117.doi: 10.1007/978-3-662-54577-5 6

    work page doi:10.1007/978-3-662-54577-5 2017

  11. [12]

    Termination of Integer Linear Programs

    M. Braverman. “Termination of Integer Linear Programs”. In:Proc. CAV ’06. LNCS 4144. 2006, pp. 372–385.doi: 10.1007/11817963 34

    work page doi:10.1007/11817963 2006

  12. [13]

    T2: Temporal Property Verification

    M. Brockschmidt, B. Cook, S. Ishtiaq, H. Khlaaf, and N. Piterman. “T2: Temporal Property Verification”. In:Proc. TACAS ’16. LNCS 9636. 2016, pp. 387–393.doi: 10.1007/978-3-662-49674-9 22

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

  13. [14]

    Analyzing Runtime and Size Complexity of Integer Programs

    M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. “Analyzing Runtime and Size Complexity of Integer Programs”. In:ACM Transactions on Programming Languages and Systems38 (2016), pp. 1–50.doi: 10. 1145/2866575

    2016

  14. [15]

    Compositional Certified Re- source Bounds

    Q. Carbonneaux, J. Hoffmann, and Z. Shao. “Compositional Certified Re- source Bounds”. In:Proc. PLDI ’15. 2015, pp. 467–478.doi: 10.1145/ 2737924.2737955. [16]ClangCompiler.url: https://clang.llvm.org/

    arXiv 2015

  15. [16]

    iRankFinder

    J. J. Dom´ enech and S. Genaim. “iRankFinder”. In:Proc. WST ’18. https: //wst2018.webs.upv.es/wst2018proceedings.pdf. 2018, p. 83

    2018

  16. [17]

    Control-Flow Refine- ment by Partial Evaluation, and its Application to Termination and Cost Analysis

    J. J. Dom´ enech, J. P. Gallagher, and S. Genaim. “Control-Flow Refine- ment by Partial Evaluation, and its Application to Termination and Cost Analysis”. In:Theory and Practice of Logic Programming19.5-6 (2019), pp. 990–1005.doi: 10.1017/S1471068419000310

    work page doi:10.1017/s1471068419000310 2019

  17. [18]

    Termination Analysis ofCPrograms Using Compiler Intermediate Languages

    S. Falke, D. Kapur, and C. Sinz. “Termination Analysis ofCPrograms Using Compiler Intermediate Languages”. In:Proc. RTA ’11. LIPIcs 10. 2011, pp. 41–50.doi: 10.4230/LIPIcs.RTA.2011.41

    work page doi:10.4230/lipics.rta.2011.41 2011

  18. [19]

    Resource Analysis of Complex Pro- grams with Cost Equations

    A. Flores-Montoya and R. H¨ ahnle. “Resource Analysis of Complex Pro- grams with Cost Equations”. In:Proc. APLAS ’14. LNCS 8858. 2014, pp. 275–295.doi: 10.1007/978-3-319-12736-1 15

    work page doi:10.1007/978-3-319-12736-1 2014

  19. [20]

    Upper and Lower Amortized Cost Bounds of Pro- grams Expressed as Cost Relations

    A. Flores-Montoya. “Upper and Lower Amortized Cost Bounds of Pro- grams Expressed as Cost Relations”. In:Proc. FM ’16. LNCS 9995. 2016, pp. 254–273.doi: 10.1007/978-3-319-48989-6 16

    work page doi:10.1007/978-3-319-48989-6 2016

  20. [21]

    A Calculus for Modular Loop Acceleration and Non-Termination Proofs

    F. Frohn and C. Fuhs. “A Calculus for Modular Loop Acceleration and Non-Termination Proofs”. In:International Journal on Software Tools for Technology Transfer24.5 (2022), pp. 691–715.doi: 10.1007/S10009-022- 00670-2. 14 N. Lommen, ´E. Meyer, J. Giesl

    work page doi:10.1007/s10009-022- 2022

  21. [22]

    Proving Non-Termination and Lower Runtime Bounds withLoAT(System Description)

    F. Frohn and J. Giesl. “Proving Non-Termination and Lower Runtime Bounds withLoAT(System Description)”. In:Proc. IJCAR ’22. LNCS 13385. 2022, pp. 712–722.doi: 10.1007/978-3-031-10769-6 41

    work page doi:10.1007/978-3-031-10769-6 2022

  22. [24]

    Improving Automatic Complexity Analysis of Integer Programs

    J. Giesl, N. Lommen, M. Hark, and F. Meyer. “Improving Automatic Complexity Analysis of Integer Programs”. In:The Logic of Software. A Tasting Menu of Formal Methods. LNCS 13360. 2022, pp. 193–228.doi: 10.1007/978-3-031-08166-8 10

    work page doi:10.1007/978-3-031-08166-8 2022

  23. [25]

    Liquidate Your Assets: Reasoning about Resource Usage inLiquid Haskell

    M. A. T. Handley, N. Vazou, and G. Hutton. “Liquidate Your Assets: Reasoning about Resource Usage inLiquid Haskell”. In:Proceedings of the ACM on Programming Languages4.POPL (2020).doi: 10.1145/3371092

    work page doi:10.1145/3371092 2020

  24. [26]

    Polynomial Loops: Beyond Termina- tion

    M. Hark, F. Frohn, and J. Giesl. “Polynomial Loops: Beyond Termina- tion”. In:Proc. LPAR ’20. EPiC 73. 2020, pp. 279–297.doi: 10.29007/ nxv1

    2020

  25. [27]

    Termination of Triangular Polynomial Loops

    M. Hark, F. Frohn, and J. Giesl. “Termination of Triangular Polynomial Loops”. In:Formal Methods in System Design65.1 (2025), pp. 70–132. doi: 10.1007/s10703-023-00440-z

    work page doi:10.1007/s10703-023-00440-z 2025

  26. [28]

    Ranking Templates for Linear Loops

    M. Heizmann and J. Leike. “Ranking Templates for Linear Loops”. In: Logical Methods in Computer Science11.1 (2015).doi: 10.2168/LMCS- 11(1:16)2015

    work page doi:10.2168/lmcs- 2015

  27. [29]

    Termination and Complexity Analysis for Programs with Bitvector Arithmetic by Symbolic Execution

    J. Hensel, J. Giesl, F. Frohn, and T. Str¨ oder. “Termination and Complexity Analysis for Programs with Bitvector Arithmetic by Symbolic Execution”. In:Journal of Logic and Algebraic Methods in Programming97 (2018), pp. 105–130.doi: 10.1016/J.JLAMP.2018.02.004

    work page doi:10.1016/j.jlamp.2018.02.004 2018

  28. [30]

    Multivariate Amortized Re- source Analysis

    J. Hoffmann, K. Aehlig, and M. Hofmann. “Multivariate Amortized Re- source Analysis”. In:ACM Transactions on Programming Languages and Systems34.3 (2012).doi: 10.1145/2362389.2362393

    work page doi:10.1145/2362389.2362393 2012

  29. [31]

    Towards Automatic Resource Bound Analysis forOCaml

    J. Hoffmann, A. Das, and S.-C. Weng. “Towards Automatic Resource Bound Analysis forOCaml”. In:Proc. POPL ’17. 2017, pp. 359–373.doi: 10.1145/3009837.3009842

    work page doi:10.1145/3009837.3009842 2017

  30. [32]

    Two Decades of Automatic Amortized Resource Analysis

    J. Hoffmann and S. Jost. “Two Decades of Automatic Amortized Resource Analysis”. In:Mathematical Structures in Computer Science32.6 (2022), pp. 729–759.doi: 10.1017/S0960129521000487

    work page doi:10.1017/s0960129521000487 2022

  31. [33]

    Termination of Linear Loops over the Integers

    M. Hosseini, J. Ouaknine, and J. Worrell. “Termination of Linear Loops over the Integers”. In:Proc. ICALP ’19. LIPIcs 132. 2019.doi: 10.4230/ LIPIcs.ICALP.2019.118

    2019

  32. [34]

    Dynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence Relations

    D. Ishimwe, K. Nguyen, and T. Nguyen. “Dynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence Relations”. In:Pro- ceedings of the ACM on Programming Languages5.OOPSLA (2021).doi: 10.1145/3485515. KoAT: Automatic Complexity and Termination Analysis of Integer Programs 15

    work page doi:10.1145/3485515 2021

  33. [35]

    Apron: A Library of Numerical Abstract Do- mains for Static Analysis

    B. Jeannet and A. Min´ e. “Apron: A Library of Numerical Abstract Do- mains for Static Analysis”. In:Proc. CAV ’09. LNCS 5643. 2009, pp. 661– 667.doi: 10.1007/978-3-642-02658-4 52. [37]KoAT: Automatic Complexity and Termination Analysis of Integer Pro- grams. Zenodo. 2026.doi: 10.5281/zenodo.18399478

    work page doi:10.1007/978-3-642-02658-4 2009

  34. [36]

    Combining Logic and Algebraic Techniques for Program Verification inTheorema

    L. Kov´ acs, N. Popov, and T. Jebelean. “Combining Logic and Algebraic Techniques for Program Verification inTheorema”. In:Proc. ISoLA ’06. 2006, pp. 67–74.doi: 10.1109/ISoLA.2006.46

    work page doi:10.1109/isola.2006.46 2006

  35. [39]

    Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs

    N. Lommen and J. Giesl. “Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs”. In:Proc. FroCoS ’23. LNCS 14279. 2023, pp. 3–22.doi: 10.1007/978-3-031-43369-6 1

    work page doi:10.1007/978-3-031-43369-6 2023

  36. [40]

    In: The Semantic Web, 6th International Se- mantic Web Conference, ISWC 2007 + ASWC 2007

    N. Lommen, ´E. Meyer, and J. Giesl. “Control-Flow Refinement for Com- plexity Analysis of Probabilistic Programs inKoAT(Short Paper)”. In: Proc. IJCAR ’24. LNCS 14739. 2024, pp. 233–243.doi: 10.1007/978-3- 031-63498-7 14

    work page doi:10.1007/978-3- 2024

  37. [42]

    Modular Automatic Complexity Analysis of Re- cursive Integer Programs

    N. Lommen and J. Giesl. “Modular Automatic Complexity Analysis of Re- cursive Integer Programs”. In:Proc. ESOP ’26. LNCS 16502. Full version available inCorrabs/2512.18851, https://doi.org/10.48550/arXiv.2512. 18851. 2026, pp. 1–31.doi: 10.1007/978-3-032-22723-2 1

    work page doi:10.48550/arxiv.2512 2026

  38. [43]

    Targeting Completeness: Automated Complexity Analysis of Integer Programs

    N. Lommen, ´E. Meyer, and J. Giesl. “Targeting Completeness: Automated Complexity Analysis of Integer Programs”. In:Journal of Automated Rea- soning70:6 (2026).doi: 10.1007/s10817-026-09751-2

    work page doi:10.1007/s10817-026-09751-2 2026

  39. [44]

    KoAT: Automatic Complexity and Termination Analysis of Integer Programs

    N. Lommen, ´E. Meyer, and J. Giesl.Experiments and Details for “KoAT: Automatic Complexity and Termination Analysis of Integer Programs”. 2026.url: https://koat.verify.rwth-aachen.de/evaluation

    2026

  40. [45]

    Interval-Based Resource Usage Verification by Translation into Horn Clauses and an Application to Energy Consumption

    P. L´ opez-Garc´ ıa, L. Darmawan, M. Klemen, U. Liqat, F. Bueno, and M. V. Hermenegildo. “Interval-Based Resource Usage Verification by Translation into Horn Clauses and an Application to Energy Consumption”. In:Theory and Practice of Logic Programming18.2 (2018), pp. 167–223.doi: 10.1017/ S1471068418000042

    2018

  41. [46]

    Ceccherini-Silberstein and M

    R. Metta, P. Yeduru, H. Karmarkar, and R. K. Medicherla. “VeriFuzz 1.4: Checking for (Non-)Termination (Competition Contribution)”. In:Proc. TACAS ’23. LNCS 13994. 2023, pp. 594–599.doi: 10.1007/978-3-031- 30820-8 42. 16 N. Lommen, ´E. Meyer, J. Giesl

    work page doi:10.1007/978-3-031- 2023

  42. [47]

    Inferring Expected Runtimes of Prob- abilistic Integer Programs Using Expected Sizes

    F. Meyer, M. Hark, and J. Giesl. “Inferring Expected Runtimes of Prob- abilistic Integer Programs Using Expected Sizes”. In:Proc. TACAS ’21. LNCS 12651. 2021, pp. 250–269.doi: 10.1007/978-3-030-72016-2 14

    work page doi:10.1007/978-3-030-72016-2 2021

  43. [49]

    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)”. In:Proc. TACAS ’25. LNCS 15698. 2025, pp. 242–247.doi: 10.1007/978-3-031-90660-2 19

    work page doi:10.1007/978-3-031-90660-2 2025

  44. [50]

    Geometric Higher Groupoids and Categories

    M. Naaf, F. Frohn, M. Brockschmidt, C. Fuhs, and J. Giesl. “Complexity Analysis for Term Rewriting by Integer Transition Systems”. In:Proc. FroCoS ’17. LNCS 10483. 2017, pp. 132–150.doi: 10.1007/978- 3- 319- 66167-4 8

    work page doi:10.1007/978- 2017

  45. [51]

    Robust Resource Bounds with Static Analysis and Bayesian Inference

    L. Pham, F. A. Saad, and J. Hoffmann. “Robust Resource Bounds with Static Analysis and Bayesian Inference”. In:Proceedings of the ACM on Programming Languages8.PLDI (2024).doi: 10.1145/3656380

    work page doi:10.1145/3656380 2024

  46. [52]

    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”. In:Proc. VMCAI ’04. LNCS 2937. 2004, pp. 239–251.doi: 10.1007/978-3-540-24622-0 20

    work page doi:10.1007/978-3-540-24622-0 2004

  47. [53]

    A Machine Learning-Based Approach for Solving Recurrence Relations and its use in Cost Analysis of Logic Programs

    L. Rustenholz, M. Klemen, M. ´A. Carreira-Perpi˜ n´ an, and P. L´ opez-Garc´ ıa. “A Machine Learning-Based Approach for Solving Recurrence Relations and its use in Cost Analysis of Logic Programs”. In:Theory and Prac- tice of Logic Programming24.6 (2024), pp. 1163–1207.doi: 10 . 1017 / S1471068424000413

    2024

  48. [54]

    Complexity and Resource Bound Anal- ysis of Imperative Programs Using Difference Constraints

    M. Sinn, F. Zuleger, and H. Veith. “Complexity and Resource Bound Anal- ysis of Imperative Programs Using Difference Constraints”. In:Journal of Automated Reasoning59.1 (2017), pp. 3–45.doi: 10.1007/s10817- 016- 9402-4

    work page doi:10.1007/s10817- 2017

  49. [55]

    Termination of Linear Programs

    A. Tiwari. “Termination of Linear Programs”. In:Proc. CAV ’04. LNCS

  50. [56]

    70–82.doi: 10.1007/978-3-540-27813-9 6

    2004, pp. 70–82.doi: 10.1007/978-3-540-27813-9 6

    work page doi:10.1007/978-3-540-27813-9 2004

  51. [57]

    TPDB (Termination Problems Data Base).url: https://github.com/ TermCOMP/TPDB-ARI

  52. [58]

    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”. In:Proceedings of the ACM on Programming Languages7.POPL (2023), pp. 2111–2140.doi: 10.1145/3571265

    work page doi:10.1145/3571265 2023

  53. [59]

    Symbolic Termination Analysis of Solvable Loops

    M. Xu and Z.-B. Li. “Symbolic Termination Analysis of Solvable Loops”. In:Journal of Symbolic Computation50 (2013), pp. 28–49.doi: 10.1016/ j.jsc.2012.05.005

    2013