There exist several results on deciding termination and computing runtime bounds for triangular weakly non-linear loops (twn-loops). We show how to use results on such subclasses of programs where complexity bounds are computable within incomplete approaches for complexity analysis of full integer programs. To this end, we present a novel modular approach which computes local runtime bounds for subprograms which can be transformed into twn-loops. These local runtime bounds are then lifted to global runtime bounds for the whole program. The power of our approach is shown by our implementation in the tool KoAT which analyzes complexity of programs where all other state-of-the-art tools fail.
翻译:决定终止和计算三角微弱的非线性环(twn-loops)的运行时间界限有几项结果。 我们展示了如何使用这类子程序分类的结果,在这些子程序分类中,复杂界限可以在不完全的方法内进行计算,以进行全整数程序的复杂性分析。 为此,我们提出了一个新型模块化方法,计算可转换为twn-loops的子程序本地运行时间界限。 然后,这些本地运行时间界限被提升到整个程序的全球运行时间界限。我们的方法的力量表现在工具KoAT中,该工具分析了所有其他最先进的工具都失败的程序的复杂性。