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.

@article{abs-1911-01077,
  title = {Inferring Lower Runtime Bounds for Integer Programs},
  author = {Florian Frohn and Matthias Naaf and Marc Brockschmidt and Jürgen Giesl},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {42},
  number = {3},
  year = {2020},
  doi = {10.1145/3410331}
}