KoAT: Automatic Complexity and Termination Analysis of Integer Programs

Nils Lommen; Éléanore Meyer; Jürgen Giesl

KoAT: Automatic Complexity and Termination Analysis of Integer Programs

Logic in Computer Science 2026-06-26 v1 Programming Languages

Authors: Nils Lommen , Éléanore Meyer , Jürgen Giesl

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.

Cite

@article{arxiv.2606.28542,
  title  = {KoAT: Automatic Complexity and Termination Analysis of Integer Programs},
  author = {Nils Lommen and Éléanore Meyer and Jürgen Giesl},
  journal= {arXiv preprint arXiv:2606.28542},
  year   = {2026}
}

Comments

CAV'26