KoAT: Automatic Complexity and Termination Analysis of Integer Programs

Lecture notes in computer science, pp. 54–69

Abstract

Abstract is a tool to automatically infer complexity bounds and prove termination of (possibly recursive) integer programs. To this end, implements an alternating modular inference of upper runtime and size bounds for program parts. In particular, uses a portfolio of different techniques to analyze subprograms. The power of our approach is demonstrated by an extensive experimental evaluation.

Authors 3

1. Nils Lommen corresponding Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

2. Fabian Meyer Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

3. Jürgen Giesl Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany