Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Nils Lommen, Fabian Meyer, Jürgen Giesl

TL;DR

A novel modular approach which computes local runtime bounds for subprograms which can be transformed into twn-loops which is implemented in the tool KoAT which analyzes complexity of programs where all other state-of-the-art tools fail.

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 KoAT which analyzes complexity of programs where all other state-of-the-art tools fail.

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

TL;DR

A novel modular approach which computes local runtime bounds for subprograms which can be transformed into twn-loops which is implemented in the tool KoAT which analyzes complexity of programs where all other state-of-the-art tools fail.

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 KoAT which analyzes complexity of programs where all other state-of-the-art tools fail.
Paper Structure (10 sections, 7 theorems, 25 equations, 4 figures, 1 algorithm)

This paper contains 10 sections, 7 theorems, 25 equations, 4 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Structure:
  3. Preliminaries
  4. Computing Global Runtime Bounds
  5. Local Runtime Bounds for Twn-Self-Loops
  6. Termination of Twn-Loops
  7. Runtime Bounds for Twn-Loops via Stabilization Thresholds
  8. Local Runtime Bounds for Twn-Cycles
  9. Conclusion and Evaluation
  10. Acknowledgments

Key Result

theorem 1

Let ${\mathcal{RB}_{\text{glo}}}$ be a global runtime bound, ${\mathcal{SB}}$ be a size bound, and $\varnothing\neq \mathcal{T}'_> \subseteq \mathcal{T}' \subseteq \mathcal{T}$ such that $\mathcal{T}'$ contains no initial transitions. Moreover, let ${\mathcal{RB}_{\text{loc}}}$ be a local runtime bo

Figures (4)

  • Figure 1: An Integer Program with a Nested Self-Loop
  • Figure 2: An Integer Program with a Nested Non-Self-Loop
  • Figure 3: Evaluation on the Collection CINT${}^+$
  • Figure : Algorithm to Compute Local Runtime Bounds for Cycles

Theorems & Definitions (23)

  • definition 1: Atoms and Formulas
  • definition 2: Integer Program
  • definition 3: Evaluation of Programs
  • definition 4: Runtime Complexity
  • definition 5: Bounds brockschmidt2016AnalyzingRuntimeSizeFestschrift
  • definition 6: Global Runtime Bound brockschmidt2016AnalyzingRuntimeSizeFestschrift
  • definition 7: Entry Transitions brockschmidt2016AnalyzingRuntimeSizeFestschrift
  • definition 8: Local Runtime Bound
  • definition 9: Size Bound brockschmidt2016AnalyzingRuntimeSizeFestschrift
  • theorem 1: Computing Global Runtime Bounds
  • ...and 13 more