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

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