Non-polynomial worst case analysis of recursive programs LNCS Chatterjee, Krishnendu ; https://orcid.org/0000-0002-4561-241X Fu, Hongfei Goharshady, Amir ; https://orcid.org/0000-0003-1702-6584 Majumdar, Rupak Kunčak, Viktor 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. Springer 2017 info:eu-repo/semantics/conferenceObject doc-type:conferenceObject text http://purl.org/coar/resource_type/c_5794 https://research-explorer.ista.ac.at/record/639 Chatterjee K, Fu H, Goharshady AK. Non-polynomial worst case analysis of recursive programs. In: Majumdar R, Kunčak V, eds. Vol 10427. Springer; 2017:41-63. doi:<a href="https://doi.org/10.1007/978-3-319-63390-9_3">10.1007/978-3-319-63390-9_3</a> eng info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-319-63390-9_3 info:eu-repo/semantics/altIdentifier/isbn/978-331963389-3 info:eu-repo/semantics/altIdentifier/wos/000431900900003 info:eu-repo/semantics/altIdentifier/arxiv/1705.00317 info:eu-repo/semantics/openAccess