Improving Automatic Complexity Analysis of Integer Programs

TL;DR

This paper enhances automatic complexity analysis of integer programs by integrating recent termination analysis techniques, leading to improved inference of runtime bounds demonstrated through extensive experiments with the KoAT tool.

Contribution

It introduces a novel integration of termination analysis methods into complexity inference, advancing the automation and accuracy of analyzing integer program runtimes.

Findings

Improved accuracy in runtime bound inference.

Successful integration of termination techniques into complexity analysis.

Extensive experimental validation with the KoAT tool.

Abstract

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.