hide
Free keywords:
Computer Science, Logic in Computer Science, cs.LO,Computer Science, Programming Languages, cs.PL
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.
