LoAT (Lower bounds Analysis Tool): 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 our tool LoAT and show that it infers non-trivial lower bounds for a large number of examples.
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Frohn, Florian; Giesl, Jürgen; Hensel, Jera; Aschermann, Cornelius; Ströder, Thomas: Lower bounds for runtime complexity of term rewriting (2017)
- Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René: Analyzing program termination and complexity automatically with \textsfAProVE (2017)
- Frohn, F.; Naaf, M.; Hensel, J.; Brockschmidt, M.; Giesl, J.: Lower runtime bounds for integer programs (2016)