article published yes Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Hongfei Fu author Amir Kafshdar Goharshady author 391365CE-F248-11E8-B48F-1D18A9856A870000-0003-1702-6584 KrCh department Efficient Algorithms for Computer Aided Verification project Rigorous Systems Engineering project Quantitative Graph Games: Theory and Applications project Quantitative Analysis of Probabilistic Systems with a focus on Crypto-Currencies project Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts project 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. ACM2019 eng 1705.00317 00056410840000110.1145/3339984 414 https://research-explorer.ista.ac.at/record/639 https://research-explorer.ista.ac.at/record/8934 Chatterjee, K., Fu, H., &#38; Goharshady, A. K. (2019). Non-polynomial worst-case analysis of recursive programs. <i>ACM Transactions on Programming Languages and Systems</i>. ACM. <a href="https://doi.org/10.1145/3339984">https://doi.org/10.1145/3339984</a> K. Chatterjee, H. Fu, A.K. Goharshady, ACM Transactions on Programming Languages and Systems 41 (2019). K. Chatterjee, H. Fu, and A. K. Goharshady, “Non-polynomial worst-case analysis of recursive programs,” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4. ACM, 2019. Chatterjee, Krishnendu, Hongfei Fu, and Amir Kafshdar Goharshady. “Non-Polynomial Worst-Case Analysis of Recursive Programs.” <i>ACM Transactions on Programming Languages and Systems</i>. ACM, 2019. <a href="https://doi.org/10.1145/3339984">https://doi.org/10.1145/3339984</a>. Chatterjee, Krishnendu, et al. “Non-Polynomial Worst-Case Analysis of Recursive Programs.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4, 20, ACM, 2019, doi:<a href="https://doi.org/10.1145/3339984">10.1145/3339984</a>. Chatterjee K, Fu H, Goharshady AK. Non-polynomial worst-case analysis of recursive programs. <i>ACM Transactions on Programming Languages and Systems</i>. 2019;41(4). doi:<a href="https://doi.org/10.1145/3339984">10.1145/3339984</a> Chatterjee K, Fu H, Goharshady AK. 2019. Non-polynomial worst-case analysis of recursive programs. ACM Transactions on Programming Languages and Systems. 41(4), 20. 70142019-11-13T08:33:43Z2026-09-13T22:31:00Z