Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs

Nils Lommen, Jürgen Giesl

TL;DR

A new procedure to infer size bounds for integer programs automatically is presented and it is shown that the technique is complete (i.e., it always computes finite size bounds) for a subclass of loops, possibly with non-linear arithmetic.

Abstract

We present a new procedure to infer size bounds for integer programs automatically. Size bounds are important for the deduction of bounds on the runtime complexity or in general, for the resource analysis of programs. We show that our technique is complete (i.e., it always computes finite size bounds) for a subclass of loops, possibly with non-linear arithmetic. Moreover, we present a novel approach to combine and integrate this complete technique into an incomplete approach to infer size and runtime bounds of general integer programs. We prove completeness of our integration for an important subclass of integer programs. We implemented our new algorithm in the automated complexity analysis tool KoAT to evaluate its power, in particular on programs with non-linear arithmetic.

Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs

TL;DR

A new procedure to infer size bounds for integer programs automatically is presented and it is shown that the technique is complete (i.e., it always computes finite size bounds) for a subclass of loops, possibly with non-linear arithmetic.

Abstract

We present a new procedure to infer size bounds for integer programs automatically. Size bounds are important for the deduction of bounds on the runtime complexity or in general, for the resource analysis of programs. We show that our technique is complete (i.e., it always computes finite size bounds) for a subclass of loops, possibly with non-linear arithmetic. Moreover, we present a novel approach to combine and integrate this complete technique into an incomplete approach to infer size and runtime bounds of general integer programs. We prove completeness of our integration for an important subclass of integer programs. We implemented our new algorithm in the automated complexity analysis tool KoAT to evaluate its power, in particular on programs with non-linear arithmetic.
Paper Structure (8 sections, 11 theorems, 22 equations, 2 figures, 1 table)

This paper contains 8 sections, 11 theorems, 22 equations, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. Size Bounds by Closed Forms
  3. Size and Runtime Bounds for Solvable Loops
  4. Closed Forms for Solvable Loops
  5. Periodic Rational Solvable Loops
  6. Size Bounds for Integer Programs
  7. Completeness of Size and Runtime Analysis for Programs
  8. Conclusion and Evaluation

Key Result

theorem 1

Let [2] $\normalfont{\texttt{cl}^{}}$ be a closed form for the loop $(\varphi, \eta)$ with start value $n_0$ and let $r\in\mathcal{B}$ be a runtime bound. Then the (absolute) size of $x\in\mathcal{V}$ is bounded by $\normalfont{\texttt{sb}^x = \lceil*\rceil{|\normalfont{\texttt{cl}^{x}}|} [n / r] +

Figures (2)

  • Figure 1: Illustration of Runtime and Size Bound Computations
  • Figure 2: An Integer Program with Non-Linear Size Bounds

Theorems & Definitions (28)

  • definition 1: Closed Forms
  • definition 2: Bounds
  • definition 3: Runtime Complexity for Loops
  • definition 4: Size Bounds for Loops
  • theorem 1: Size Bounds for Loops with Closed Forms
  • definition 5: Solvable Update solvable-mapsxuSymbolicTerminationAnalysis2013kincaidClosedFormsNumerical2019frohn2020TerminationPolynomialLoopskovacsReasoningAlgebraicallyPSolvable2008DBLP:conf/vmcai/HumenbergerJK18
  • definition 6: TWN-Update frohn2020TerminationPolynomialLoopshark2020PolynomialLoopsTerminationfrohn2019TerminationTriangularInteger
  • lemma 1: Transforming Solvable Updates (see frohn2020TerminationPolynomialLoops)
  • lemma 2: Closed Forms for TWN-Updates (see frohn2019TerminationTriangularInteger)
  • theorem 2: Closed Forms for Solvable Updates
  • ...and 18 more