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.

翻译：本文提出了一种自动推断整数程序规模界限的新方法。规模界限对于推导程序运行时复杂度界限乃至程序资源分析至关重要。我们证明该技术对于可能包含非线性算术的循环子类具有完备性（即总能计算出有限规模界限）。此外，我们提出了一种创新方案，将这种完备性技术与推断通用整数程序规模及运行时界限的非完备方法进行融合集成。针对整数程序的重要子类，我们证明了该集成方法的完备性。我们在自动化复杂度分析工具KoAT中实现了新算法，并通过评估验证了其效能，特别是在处理非线性算术程序方面。