@article{7014,
  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
nonrecursive programs. First, we apply ranking functions to recursion,
resulting in measure functions. We show that measure functions 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
nonpolynomial 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 $\mathcal{O}(n\log n)$
as well as $\mathcal{O}(n^r)$ where $r$ is not an integer. We present
experimental results to demonstrate that our approach can obtain efficiently
worst-case bounds of classical recursive algorithms such as (i) Merge-Sort, the
divide-and-conquer algorithm for the Closest-Pair problem, where we obtain
$\mathcal{O}(n \log n)$ worst-case bound, and (ii) Karatsuba's algorithm for
polynomial multiplication and Strassen's algorithm for matrix multiplication,
where we obtain $\mathcal{O}(n^r)$ bound such that $r$ is not an integer and
close to the best-known bounds for the respective algorithms.},
  author       = {Chatterjee, Krishnendu and Fu, Hongfei and Goharshady, Amir Kafshdar},
  journal      = {ACM Transactions on Programming Languages and Systems},
  number       = {4},
  publisher    = {ACM},
  title        = {{Non-polynomial worst-case analysis of recursive programs}},
  doi          = {10.1145/3339984},
  volume       = {41},
  year         = {2019},
}