---
res:
bibo_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.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Krishnendu
foaf_name: Chatterjee, Krishnendu
foaf_surname: Chatterjee
foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4561-241X
- foaf_Person:
foaf_givenName: Hongfei
foaf_name: Fu, Hongfei
foaf_surname: Fu
- foaf_Person:
foaf_givenName: Amir
foaf_name: Goharshady, Amir
foaf_surname: Goharshady
foaf_workInfoHomepage: http://www.librecat.org/personId=391365CE-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0003-1702-6584
bibo_doi: 10.1007/978-3-319-63390-9_3
bibo_volume: 10427
dct_date: 2017^xs_gYear
dct_isPartOf:
- http://id.crossref.org/issn/978-331963389-3
dct_language: eng
dct_publisher: Springer@
dct_title: Non-polynomial worst case analysis of recursive programs@
...