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