In earlier work, we developed an approach for automatic complexity analysis of integer programs, based on an alternating modular inference of upper runtime and size bounds for program parts. In this paper, we show how recent techniques to improve automated termination analysis of integer programs (like the generation of multiphase-linear ranking functions and control-flow refinement) can be integrated into our approach for the inference of runtime bounds. The power of the resulting approach is demonstrated by an extensive experimental evaluation with our new re-implementation of the corresponding tool KoAT.
翻译:在早期工作中,我们根据对程序部件的上运行时间和大小界限的交替模块式推论,制定了对整数程序进行自动复杂分析的方法。在本文中,我们展示了如何将改进整数程序自动终止分析的最新技术(如生成多阶段线性排位函数和控制流量改进)纳入我们计算运行时间界限的方法中。由此得出的方法的力量通过我们重新采用相应的 KoAT 工具的大规模实验性评估得到证明。