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

arXiv: https://arxiv.org/abs/2307.06921 · HTML: https://mlsanity.com/paper/2307.06921/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Jul 2023.

## Built on by (most cited first, 1 of 1)

- [A Machine Learning-based Approach for Solving Recurrence Relations and its use in Cost Analysis of Logic Programs](https://mlsanity.com/paper/2405.06972/) (2024)

## Abstract (arXiv)

We present a new procedure to infer size bounds for integer programs automatically. Size bounds are important for the deduction of bounds on the runtime complexity or in general, for the resource analysis of programs. We show that our technique is complete (i.e., it always computes finite size bounds) for a subclass of loops, possibly with non-linear arithmetic. Moreover, we present a novel approach to combine and integrate this complete technique into an incomplete approach to infer size and runtime bounds of general integer programs. We prove completeness of our integration for an important subclass of integer programs. We implemented our new algorithm in the automated complexity analysis tool KoAT to evaluate its power, in particular on programs with non-linear arithmetic.