We present a modular approach to automatic complexity analysis of integer programs. Based on a novel alternation between finding symbolic time bounds for program parts and using these to infer bounds on the absolute values of program variables, we can restrict each analysis step to a small part of the program while maintaining a high level of precision. The bounds computed by our method are polynomial or exponential expressions that depend on the absolute values of input parameters.ududWe show how to extend our approach to arbitrary cost measures, allowing to use our technique to find upper bounds for other expended resources, such as network requests or memory consumption. Our contributions are implemented in the open source tool KoAT, and extensive experiments show the performance and power of our implementation in comparison with other tools.
展开▼
机译：我们提出了一种用于整数程序自动复杂度分析的模块化方法。基于为程序部分找到符号时间界限并使用它们推断程序变量绝对值的界限之间的新颖替代，我们可以将每个分析步骤限制在程序的一小部分，同时保持较高的精度。我们的方法计算出的界限是取决于输入参数绝对值的多项式或指数表达式。 ud ud我们展示了如何将我们的方法扩展到任意成本度量，从而允许使用我们的技术来查找其他消耗资源的上限，例如网络请求或内存消耗。我们的贡献是在开源工具KoAT中实现的，并且广泛的实验证明了与其他工具相比，我们实现的性能和力量。
展开▼
