English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Paper

Inferring Lower Runtime Bounds for Integer Programs

MPS-Authors
/persons/resource/persons253052

Frohn,  Florian
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (public)

arXiv:1911.01077.pdf
(Preprint), 947KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Frohn, F., Naaf, M., Brockschmidt, M., & Giesl, J. (2019). Inferring Lower Runtime Bounds for Integer Programs. Retrieved from https://arxiv.org/abs/1911.01077.


Cite as: http://hdl.handle.net/21.11116/0000-0007-CEF3-F
Abstract
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.