论文标题
通过三角形弱非线性环对整数程序进行自动复杂性分析
Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
论文作者
论文摘要
决定终止和计算三角形弱非线性环（TWN-loops）的运行时边界有几个结果。我们展示了如何在此类程序的子类上使用结果，在这些程序的子类中，在不完整的方法中可以计算复杂性界限，以实现完整整数程序的复杂性分析。为此，我们提出了一种新型的模块化方法，该方法计算可转换为TWN环的子程序的局部运行时边界。然后将这些本地运行时范围提起到整个程序的全局运行时界。我们在工具中的实现显示了我们方法的力量，该工具分析了所有其他最先进工具失败的程序的复杂性。
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.
