Non-polynomial worst case analysis of recursive programs Conference Paper

Author(s): Chatterjee, Krishnendu; Fu, Hongfei; Goharshady, Amir K
Title: Non-polynomial worst case analysis of recursive programs
Title Series: LNCS
Affiliation IST Austria
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 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.
Conference Title: CAV: Computer Aided Verification
Volume: 10427
Conference Dates: July 24 - 28, 2017
Conference Location: Heidelberg, Germany
Publisher: Springer  
Date Published: 2017-01-01
Start Page: 41
End Page: 63
Sponsor: Vienna Science and Technology Fund (WWTF) ICT15-003, Austrian Science Fund (FWF) NFN Grant No. S11407-N23 (RiSE/SHiNE), ERC Start grant (279307), the Natural Science Foundation of China (NSFC) under Grant No. 61532019, CDZ project CAP (GZ 1023)
DOI: 10.1007/978-3-319-63390-9_3
Notes: We thank all reviewers for valuable comments.
Open access: yes (repository)