English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse
  1. View item / 
  2. Item Summary

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

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 (restricted access)
There are currently no full texts shared for your IP range.
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: https://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.