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

TL;DR

This paper introduces a new complete method for automatically inferring size bounds of integer programs, including those with non-linear arithmetic, and integrates it into an existing analysis tool to improve resource and runtime bounds estimation.

Contribution

It presents a novel complete technique for size bounds inference in integer programs and a method to integrate it with incomplete approaches, enhancing analysis capabilities.

Findings

The technique is complete for a subclass of loops with non-linear arithmetic.

The integrated approach is complete for a significant class of integer programs.

Implementation in KoAT demonstrates improved analysis of non-linear programs.

Abstract

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.