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

Lecture notes in computer science, pp. 3–22

Abstract

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 to evaluate its power, in particular on programs with non-linear arithmetic.

Authors 2

1. Nils Lommen corresponding Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2, RWTH Aachen University, Aachen, Germany

2. Jürgen Giesl corresponding Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2, RWTH Aachen University, Aachen, Germany