Empirical Evaluation of: Lower Runtime Bounds for Integer Programs

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.

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 ("Final Cost" resp. "Final 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-static test. The proof attempt is then printed on the screen.

Input Format

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

Restrictions

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.

References