---
_id: '639'
abstract:
- lang: eng
  text: 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.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Hongfei
  full_name: Fu, Hongfei
  last_name: Fu
- first_name: Amir
  full_name: Goharshady, Amir
  id: 391365CE-F248-11E8-B48F-1D18A9856A87
  last_name: Goharshady
  orcid: 0000-0003-1702-6584
citation:
  ama: '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:<a
    href="https://doi.org/10.1007/978-3-319-63390-9_3">10.1007/978-3-319-63390-9_3</a>'
  apa: 'Chatterjee, K., Fu, H., &#38; Goharshady, A. K. (2017). Non-polynomial worst
    case analysis of recursive programs. In R. Majumdar &#38; 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>'
  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. <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>.
  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.'
  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.'
  mla: 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>.
  short: K. Chatterjee, H. Fu, A.K. Goharshady, in:, R. Majumdar, V. Kunčak (Eds.),
    Springer, 2017, pp. 41–63.
conference:
  end_date: 2017-07-28
  location: Heidelberg, Germany
  name: 'CAV: Computer Aided Verification'
  start_date: 2017-07-24
date_created: 2018-12-11T11:47:39Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2025-06-02T08:53:47Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-319-63390-9_3
ec_funded: 1
editor:
- first_name: Rupak
  full_name: Majumdar, Rupak
  last_name: Majumdar
- first_name: Viktor
  full_name: Kunčak, Viktor
  last_name: Kunčak
external_id:
  arxiv:
  - '1705.00317'
intvolume: '     10427'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1705.00317
month: '01'
oa: 1
oa_version: Submitted Version
page: 41 - 63
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
  isbn:
  - 978-331963389-3
publication_status: published
publisher: Springer
publist_id: '7149'
quality_controlled: '1'
related_material:
  record:
  - id: '8934'
    relation: dissertation_contains
    status: public
  - id: '7014'
    relation: later_version
    status: public
scopus_import: 1
status: public
title: Non-polynomial worst case analysis of recursive programs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10427
year: '2017'
...