整数程序的自动复杂性分析通过三角形弱非线性循环
摘要：关于决定终止和计算运行时界限的三角形弱非线性循环（twn-loops）存在几个结果。我们展示了如何使用此类程序的子类的结果，在其中复杂性界限可以在完全的整数程序复杂性分析中计算得出不完全的方法。为此，我们提出了一种新颖的模块化方法，它计算可以转化为twn-loops的子程序的本地运行时界限。然后，这些本地运行时界限被提升为整个程序的全局运行时界限。我们的方法的强大之处在于我们在KoAT工具中的实现，该工具分析其它所有最先进工具均无法处理的程序的复杂性。
作者：Nils Lommen, Fabian Meyer, J"urgen Giesl
论文ID：2205.08869
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-06