针对完整性：使用闭式形式进行整数程序的大小界限
摘要：自动推断整数程序的大小界限是一种新的过程。大小界限对于推导运行时复杂性的界限或者一般情况下的程序资源分析非常重要。我们展示了我们的技术在循环的一个子类上是完整的（即总是计算出有限的大小界限），即使循环中包含了非线性算术。此外，我们提出了一种将这种完整技术与不完整方法相结合和整合的新方法，用于推断整数程序的大小和运行时界限。我们证明了我们集成的完整性对于整数程序的一个重要子类。我们在自动复杂性分析工具KoAT中实施了我们的新算法，以评估其能力，尤其是对于包含非线性算术的程序。
作者：Nils Lommen, J"urgen Giesl
论文ID：2307.06921
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-14