@inproceedings{639,
  abstract     = {We study the problem of developing efficient approaches for proving worst-case bounds of non-deterministic recursive programs. Ranking functions are sound and complete for proving termination and worst-case bounds of non-recursive programs. First, we apply ranking functions to recursion, resulting in measure functions, and show that they provide a sound and complete approach to prove worst-case bounds of non-deterministic recursive programs. Our second contribution is the synthesis of measure functions in non-polynomial forms. We show that non-polynomial measure functions with logarithm and exponentiation can be synthesized through abstraction of logarithmic or exponentiation terms, Farkas’ Lemma, and Handelman’s Theorem using linear programming. While previous methods obtain worst-case polynomial bounds, our approach can synthesize bounds of the form O(n log n) as well as O(nr) where r is not an integer. We present experimental results to demonstrate that our approach can efficiently obtain worst-case bounds of classical recursive algorithms such as Merge-Sort, Closest-Pair, Karatsuba’s algorithm and Strassen’s algorithm.},
  author       = {Chatterjee, Krishnendu and Fu, Hongfei and Goharshady, Amir},
  editor       = {Majumdar, Rupak and Kunčak, Viktor},
  isbn         = {978-331963389-3},
  location     = {Heidelberg, Germany},
  pages        = {41 -- 63},
  publisher    = {Springer},
  title        = {{Non-polynomial worst case analysis of recursive programs}},
  doi          = {10.1007/978-3-319-63390-9_3},
  volume       = {10427},
  year         = {2017},
}