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.
Our detailed experimental evaluation is on a second page.
The table with the results of the evaluation also shows the concrete bounds computed by LoAT. However, note
that such a concrete bound only applies if the corresponding guard is satisfied. To see
the guard, follow
the link output
to get LoAT's full proof. There, cost and guard of
the transition that proves the lower bound inferred by LoAT are shown at the end
of the proof ("Solved Cost
" resp. "Rule Guard
").
To run the binary on an example file test
, execute the
command loat_0566b test
. The proof attempt is then printed on
the screen. By default, all novel contributions of our paper "Inferring Lower
Runtime Bounds for Integer Programs" are enabled, resulting in the most
powerful configuration of LoAT. To test our novel contributions individually,
use the command loat_0566b --benchmark x test
and
set x
to:
basic
to disable all novel contributionscond
to disable all novel contributions except for conditional metering functionsrec
to disable all novel contributions except for the handling of
possibly non-tail-recursive programssmt
to disable all novel contributions except for the SMT encoding of limit problems, which
is used in addition to our calculus to solve limit problems (see Section 6 of our paper for
more details on the integration of our SMT encoding into our calculus for limit problems)just-smt
to disable all novel contributions except for the SMT encoding of limit problems,
which is used exclusively as soon as it is applicableThe input format of LoAT is an extension of the input format of KoAT. The only difference is that rules can be annotated with costs, where LoAT currently only supports polynomial costs. An example for such cost annotations is:
l1(A,B) -{A^2,A^2+B}> Com_2(l2(A,B),l3(A,B)) :|: B >= 0
A^2
is a lower bound on the cost of the rule and A^2+B
is an
upper bound on the cost of the rule. The upper bound is ignored by LoAT. The lower bound has
to be non-negative for every model of the transition's guard.
Here is the preliminary version "Lower Runtime Bounds for Integer Programs" which appeared in the proceedings of IJCAR '16.
As mentioned in our paper, Lemma 5.8 is an adaption of Lemma 24 from our paper "Lower Bounds for Runtime Complexity of Term Rewriting" which appeared in the Journal of Automated Reasoning.