Inferring Lower Runtime Bounds for Integer Programs

TL;DR

This paper introduces a novel technique for inferring lower bounds on the worst-case runtime of integer programs, extending previous methods by handling non-tail-recursive cases through symbolic execution and program acceleration.

Contribution

It presents a new approach combining symbolic execution, recurrence solving, and SMT encoding to infer lower bounds for a broad class of integer programs, not limited to tail-recursive ones.

Findings

Successfully infers non-trivial lower bounds for various examples

Extends analysis capabilities beyond tail-recursive programs

Implemented in the LoAT tool with promising results

Abstract

We present a technique to infer lower bounds on the worst-case runtime complexity of integer programs, where in contrast to earlier work, our approach is not restricted to tail-recursion. Our technique constructs symbolic representations of program executions using a framework for iterative, under-approximating program simplification. The core of this simplification is a method for (under-approximating) program acceleration based on recurrence solving and a variation of ranking functions. Afterwards, we deduce asymptotic lower bounds from the resulting simplified programs using a special-purpose calculus and an SMT encoding. We implemented our technique in our tool LoAT and show that it infers non-trivial lower bounds for a large class of examples.