Non-polynomial worst case analysis of recursive programs
LNCS
published
yes
Krishnendu
Chatterjee
author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X
Hongfei
Fu
author
Amir
Goharshady
author 391365CE-F248-11E8-B48F-1D18A9856A870000-0003-1702-6584
RupakMajumdar
editor
ViktorKunčak
editor
KrCh
department
CAV: Computer Aided Verification
Game Theory
project
Quantitative Graph Games: Theory and Applications
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 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.
Springer2017Heidelberg, Germany
eng
978-331963389-310.1007/978-3-319-63390-9_3
1042741 - 63
Chatterjee K, Fu H, Goharshady A. 2017. Non-polynomial worst case analysis of recursive programs. CAV: Computer Aided Verification, LNCS, vol. 10427. 41–63.
K. Chatterjee, H. Fu, and A. Goharshady, “Non-polynomial worst case analysis of recursive programs,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10427, pp. 41–63.
K. Chatterjee, H. Fu, A. Goharshady, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 41–63.
Chatterjee, K., Fu, H., & Goharshady, A. (2017). Non-polynomial worst case analysis of recursive programs. In R. Majumdar & V. Kunčak (Eds.) (Vol. 10427, pp. 41–63). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. <a href="https://doi.org/10.1007/978-3-319-63390-9_3">https://doi.org/10.1007/978-3-319-63390-9_3</a>
Chatterjee, Krishnendu, Hongfei Fu, and Amir Goharshady. “Non-Polynomial Worst Case Analysis of Recursive Programs.” edited by Rupak Majumdar and Viktor Kunčak, 10427:41–63. Springer, 2017. <a href="https://doi.org/10.1007/978-3-319-63390-9_3">https://doi.org/10.1007/978-3-319-63390-9_3</a>.
Chatterjee K, Fu H, Goharshady A. 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>
Chatterjee, Krishnendu, et al. <i>Non-Polynomial Worst Case Analysis of Recursive Programs</i>. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer, 2017, pp. 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>.
6392018-12-11T11:47:39Z2019-08-02T12:39:19Z