We present a technique to infer lower bounds on the worst-case runtime complexity of integer programs. To this end, we construct 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.
We implemented our technique in the open-source tool LoAT and extensive experiments show the performance and power of our implementation.
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 ("Final Cost
" resp. "Final Guard
").
To run the binary on an example file test
,
execute the command LoAT-static test
. The proof attempt is then
printed on the screen.
The input format of LoAT is equal to
the input format
of KoAT. However, LoAT currently just supports transitions
with one end state (i.e., just Com_1
is supported). Hence, the end
state need not be wrapped in Com_1(...)
(i.e., Com_1(f(x,y))
can be
abbreviated by f(x,y)
).
While the technique presented in "Lower Runtime Bounds for Integer Programs" is able to infer exponential lower bounds as well as polynomial bounds with rational exponents, LoAT currently just supports exponential bounds and polynomial bounds with natural exponents.
Moreover, the cost of each transition in the initial program is one, i.e., user-defined costs are currently not supported in the implementation.
LoAT's development was inspired by the tool KoAT. KoAT is the implementation corresponding to our paper "Alternating Runtime and Size Complexity Analysis of Integer Programs" which appeared at TACAS '14. An extended and revised version of this paper called "Analyzing Runtime and Size Complexity of Integer Programs" will appear in the ACM Transactions on Programming Languages and Systems.
As mentioned in our paper, Lemma 17 is an adaption of Lemma 18 from our paper "Inferring Lower Bounds for Runtime Complexity" which appeared at RTA '15.