[{"editor":[{"last_name":"Majumdar","first_name":"Rupak"},{"last_name":"Kunčak","first_name":"Viktor"}],"author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Hongfei","last_name":"Fu"},{"last_name":"Goharshady","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir"}],"publist_id":"7149","external_id":{"arxiv":[]},"article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","dini_type":"doc-type:conferenceObject","citation":{"mla":"Chatterjee, Krishnendu, et al. Non-Polynomial Worst Case Analysis of Recursive Programs. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer, 2017, pp. 41–63, doi:10.1007/978-3-319-63390-9_3.","apa":"Chatterjee, K., Fu, H., & Goharshady, A. K. (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. https://doi.org/10.1007/978-3-319-63390-9_3","short":"K. Chatterjee, H. Fu, A.K. Goharshady, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 41–63.","ieee":"K. Chatterjee, H. Fu, and A. K. Goharshady, “Non-polynomial worst case analysis of recursive programs,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10427, pp. 41–63.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Amir Kafshdar Goharshady. “Non-Polynomial Worst Case Analysis of Recursive Programs.” edited by Rupak Majumdar and Viktor Kunčak, 10427:41–63. Springer, 2017. https://doi.org/10.1007/978-3-319-63390-9_3.","ista":"Chatterjee K, Fu H, Goharshady AK. 2017. Non-polynomial worst case analysis of recursive programs. CAV: Computer Aided Verification, LNCS, vol. 10427, 41–63."},"project":[{"name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"date_published":"2017-01-01T00:00:00Z","date_created":"2018-12-11T11:47:39Z","uri_base":"https://research-explorer.ista.ac.at","page":"41 - 63","day":"01","dc":{"date":["2017"],"type":["info:eu-repo/semantics/conferenceObject","doc-type:conferenceObject","text","http://purl.org/coar/resource_type/c_5794"],"publisher":["Springer"],"relation":["info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-319-63390-9_3","info:eu-repo/semantics/altIdentifier/isbn/978-331963389-3","info:eu-repo/semantics/altIdentifier/arxiv/1705.00317","info:eu-repo/grantAgreement/FWF//S11407","info:eu-repo/grantAgreement/EC/FP7/279307"],"source":["Chatterjee K, Fu H, Goharshady AK. Non-polynomial worst case analysis of recursive programs. In: Majumdar R, Kunčak V, eds. Vol 10427. Springer; 2017:41-63. doi:10.1007/978-3-319-63390-9_3"],"identifier":["https://research-explorer.ista.ac.at/record/639"],"description":["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."],"title":["Non-polynomial worst case analysis of recursive programs","LNCS"],"rights":["info:eu-repo/semantics/openAccess"],"language":["eng"],"creator":["Chatterjee, Krishnendu","Fu, Hongfei","Goharshady, Amir","Majumdar, Rupak","Kunčak, Viktor"]},"quality_controlled":"1","oa":1,"department":[{"tree":[{"_id":"ResearchGroups"},{"_id":"IST"}],"_id":"KrCh"}],"creator":{"login":"apreinsp","id":"4435EBFC-F248-11E8-B48F-1D18A9856A87"},"date_updated":"2024-03-27T23:30:33Z","status":"public","type":"conference","conference":{"end_date":"2017-07-28","location":"Heidelberg, Germany","start_date":"2017-07-24","name":"CAV: Computer Aided Verification"},"_id":"639","volume":10427,"related_material":{"record":[{"relation":"later_version","id":"7014","status":"public"},{"id":"8934","status":"public","relation":"dissertation_contains"}]},"ec_funded":1,"language":[{}],"publication_identifier":{"isbn":[]},"publication_status":"published","month":"01","intvolume":" 10427","scopus_import":1,"alternative_title":[],"main_file_link":[{"url":"https://arxiv.org/abs/1705.00317","open_access":"1"}],"oa_version":"Submitted Version","abstract":[{"lang":"eng"}]}]