2022/02/03 by Jürgen Giesl, Giesl, Jürgen, Nils Lommen +5 · 1 citation
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Software Engineering Research
paper · pdf · doi:10.48550/arxiv.2202.01769
openalex publication_date 2022/02/03 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.