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.


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:

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