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中，以评估其能力，特别是在处理包含非线性算术的程序时。