{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T08:19:06Z","timestamp":1772785146447,"version":"3.50.1"},"reference-count":72,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2019,10,12]],"date-time":"2019-10-12T00:00:00Z","timestamp":1570838400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"crossref","award":["ICT15-003"],"award-info":[{"award-number":["ICT15-003"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"crossref"}]},{"name":"ERC","award":["279307 (Graph Games)"],"award-info":[{"award-number":["279307 (Graph Games)"]}]},{"name":"DOC Fellowship of the Austrian Academy of Sciences"},{"name":"Austrian Science Fund (FWF) NFN","award":["S11407-N23 (RiSE\/SHiNE)"],"award-info":[{"award-number":["S11407-N23 (RiSE\/SHiNE)"]}]},{"DOI":"10.13039\/501100001809","name":"Natural Science Foundation of China","doi-asserted-by":"crossref","award":["61532019 and 61802254"],"award-info":[{"award-number":["61532019 and 61802254"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"CDZ project CAP"},{"name":"IBM Ph.D.Fellowship program"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2019,12,31]]},"abstract":"<jats:p>\n            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. We show that measure functions 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\u2019s Theorem using linear programming. While previous methods obtain polynomial worst-case bounds, our approach can synthesize bounds of various forms including O(\n            <jats:italic>n<\/jats:italic>\n            log\n            <jats:italic>n<\/jats:italic>\n            ) and O(\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>\n              <jats:italic>r<\/jats:italic>\n            <\/jats:sup>\n            ), where\n            <jats:italic>r<\/jats:italic>\n            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 (i)\u00a0Merge sort, Heap sort, and the divide-and-conquer algorithm for the Closest Pair problem, where we obtain O(\n            <jats:italic>n<\/jats:italic>\n            log\n            <jats:italic>n<\/jats:italic>\n            ) worst-case bound, and (ii)\u00a0Karatsuba\u2019s algorithm for polynomial multiplication and Strassen\u2019s algorithm for matrix multiplication, for which we obtain O(\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>\n              <jats:italic>r<\/jats:italic>\n            <\/jats:sup>\n            ) bounds such that\n            <jats:italic>r<\/jats:italic>\n            is not an integer and is close to the best-known bound for the respective algorithm. Besides the ability to synthesize non-polynomial bounds, we also show that our approach is equally capable of obtaining polynomial worst-case bounds for classical programs such as Quick sort and the dynamic programming algorithm for computing Fibonacci numbers.\n          <\/jats:p>","DOI":"10.1145\/3339984","type":"journal-article","created":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T16:35:58Z","timestamp":1571157358000},"page":"1-52","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Non-polynomial Worst-Case Analysis of Recursive Programs"],"prefix":"10.1145","volume":"41","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[{"name":"IST Austria (Institute of Science and Technology Austria), Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongfei","family":"Fu","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, P.R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,10,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.12.008"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_15"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_12"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_7"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_19"},{"key":"e_1_2_1_7_1","volume-title":"Sherbert","author":"Bartle Robert G.","year":"2011","unstructured":"Robert G. Bartle and Donald R. Sherbert. 2011. Introduction to Real Analysis (4th ed.). John Wiley 8 Sons, Inc."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2866575"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_3"},{"key":"e_1_2_1_16_1","volume-title":"Amir Kafshdar Goharshady, and Ehsan Kafshdar Goharshady","author":"Chatterjee Krishnendu","year":"2019","unstructured":"Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Ehsan Kafshdar Goharshady. 2019. Polynomial invariant generation for non-deterministic recursive programs. CoRR abs\/1902.04373 (2019). arxiv:1902.04373 http:\/\/arxiv.org\/abs\/1902.04373."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","unstructured":"Krishnendu Chatterjee Hongfei Fu Petr Novotn\u00fd and Rouzbeh Hasheminezhad. 2016. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs See Reference Bod\u00edk and Majumdar [8] 327--342. DOI:https:\/\/doi.org\/10.1145\/2837614.2837639","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","unstructured":"Krishnendu Chatterjee Petr Novotn\u00fd and \u0110or\u0111e \u017dikeli\u0107. 2017. Stochastic invariants for probabilistic termination See Reference Castagna and Gordon [12] 145--160. DOI:https:\/\/doi.org\/10.1145\/3009837","DOI":"10.1145\/3009837"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1012996816178"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_6"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0087-8"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"e_1_2_1_25_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H.","unstructured":"Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms (3rd ed.). MIT Press.","edition":"3"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103687"},{"key":"e_1_2_1_29_1","volume-title":"A Fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian). Math. Term. \u00c9rtesit\u00f6 12","author":"Farkas J.","year":"1894","unstructured":"J. Farkas. 1894. A Fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian). Math. Term. \u00c9rtesit\u00f6 12 (1894), 457--472."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90145-R"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Robert W. Floyd. 1967. Assigning meanings to programs. Mathematical Aspects of Computer Science (Proceedings of a Symposium in Applied Mathematics) J. T. Schwarz (Ed.) 19 (1967) 19--32.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_22"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","unstructured":"St\u00e9phane Gimenez and Georg Moser. 2016. The complexity of interaction See Reference Bod\u00edk and Majumdar [8] 243--255. DOI:https:\/\/doi.org\/10.1145\/2837614.2837646","DOI":"10.1145\/2837614.2837646"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.2307\/2274987"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507666"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_35"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_7"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480898"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1988.132.35"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211249"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17164-2_13"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_3"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_24"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317785"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_2_1_51_1","unstructured":"Claire Jones. 1989. Probabilistic Non-Determinism. Ph.D. Dissertation. The University of Edinburgh."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706327"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_23"},{"key":"e_1_2_1_54_1","volume-title":"The Art of Computer Programming","author":"Knuth Donald E.","unstructured":"Donald E. Knuth. 1973. The Art of Computer Programming, Volume I--III. Addison-Wesley."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_21"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1498926.1498928"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_2_1_58_1","unstructured":"lpsolve 2016. lp_solve 5.5.2.3. Retrieved from http:\/\/lpsolve.sourceforge.net\/5.5\/."},{"key":"e_1_2_1_59_1","unstructured":"Martin Lukasiewycz. 2008. Java ILP\u2014Java Interface to ILP Solvers. Retrieved from http:\/\/javailp.sourceforge.net\/."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_7"},{"key":"e_1_2_1_63_1","volume-title":"Theory of Linear and Integer Programming","author":"Schrijver Alexander","unstructured":"Alexander Schrijver. 1999. Theory of Linear and Integer Programming. Wiley."},{"key":"e_1_2_1_64_1","volume-title":"Combinatorial Optimization\u2014Polyhedra and Efficiency","author":"Schrijver Alexander","unstructured":"Alexander Schrijver. 2003. Combinatorial Optimization\u2014Polyhedra and Efficiency. Springer."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11424-013-1004-1"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73228-0_25"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/113413.113433"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_5"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347389"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-009-0074-7"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3339984","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3339984","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:26:11Z","timestamp":1750206371000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3339984"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,12]]},"references-count":72,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,12,31]]}},"alternative-id":["10.1145\/3339984"],"URL":"https:\/\/doi.org\/10.1145\/3339984","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,12]]},"assertion":[{"value":"2017-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-10-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}