10.1007/978-3-319-63390-9_3
Chatterjee, Krishnendu
Krishnendu
Chatterjee0000-0002-4561-241X
Fu, Hongfei
Hongfei
Fu
Goharshady, Amir
Amir
Goharshady0000-0003-1702-6584
Majumdar, Rupak
Rupak
Majumdar
Kunčak, Viktor
Viktor
Kunčak
Non-polynomial worst case analysis of recursive programs
LNCS
Springer
2017
2018-12-11T11:47:39Z
2020-07-14T12:47:47Z
conference
https://research-explorer.app.ist.ac.at/record/639
https://research-explorer.app.ist.ac.at/record/639.json
978-331963389-3
1705.00317
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.