Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops

Lecture notes in computer science, pp. 734–754

Abstract

Abstract There exist several results on deciding termination and computing runtime bounds for triangular weakly non-linear loops (twn-loops). We show how to use results on such subclasses of programs where complexity bounds are computable within incomplete approaches for complexity analysis of full integer programs. To this end, we present a novel modular approach which computes local runtime bounds for subprograms which can be transformed into twn-loops. These local runtime bounds are then lifted to global runtime bounds for the whole program. The power of our approach is shown by our implementation in the tool $$\textsf {KoAT}$$ KoAT which analyzes complexity of programs where all other state-of-the-art tools fail.

Authors 3

1. Nils Lommen corresponding Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2, RWTH Aachen University, Aachen, Germany

2. Fabian Meyer Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2, RWTH Aachen University, Aachen, Germany

3. Jürgen Giesl corresponding Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2, RWTH Aachen University, Aachen, Germany