论文标题

改善整数程序的自动复杂性分析

Improving Automatic Complexity Analysis of Integer Programs

论文作者

Giesl, Jürgen, Lommen, Nils, Hark, Marcel, Meyer, Fabian

论文摘要

在较早的工作中,我们基于对程序零件的上运行时和大小范围的交替推理进行了一种自动复杂性分析的方法。在本文中,我们展示了如何改善整数程序的自动终止分析(例如生成多相线性排名函数和控制流的细化)如何集成到我们的方法中,以推断运行时界限。通过广泛的实验评估,我们对相应的工具KOAT的重新实现进行了广泛的实验评估,证明了所得方法的功能。

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.

扫码加入交流群

加入微信交流群

微信交流群二维码

扫码加入学术交流群,获取更多资源