Empirical Evaluation of: Inferring Lower Runtime Bounds for Integer Programs

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.

Experimental Evaluation

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").

Example Set

For the evaluation, we used the example sets listed here. You can find all examples on github.

Implementation

Our implementation LoAT is available on github. You can also download a pre-compiled binary for Linux/x64.

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 contributions
cond to disable all novel contributions except for conditional metering functions
rec to disable all novel contributions except for the handling of possibly non-tail-recursive programs
smt 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 applicable

Input Format

The 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

Here, 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.

Examples from the Paper

Fibonacci (Example 2.1)	LoAT's output
Leading example (Figure 1)	LoAT's output
Program with unbounded cost due to a temporary variable in a cost expression (Example 2.7)	LoAT's output
Program with unbounded cost due to a temporary variable on the right-hand side (Example 2.7)	LoAT's output
Motivating example for conditional metering functions (Example 3.5)	LoAT's output
Example to illustrate how to handle non-terminating programs with conditional metering functions (Example 3.6)	LoAT's output
Example with exponential growth of data (Example 3.9)	LoAT's output
Motivating example for partial deletion (Example 4.8)	LoAT's output
FacSum example (Example 4.9)	LoAT's output
Example to illustrate the inference of sub-linear bounds (Example 5.1)	LoAT's output

References

Here is a link to our paper "Inferring Lower Runtime Bounds for Integer Programs".
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.