---
_id: '5446'
abstract:
- lang: eng
text: "We study the problem of developing efficient approaches for proving termination
of recursive programs with one-dimensional arrays. Ranking functions serve as
a sound and complete approach for proving termination of non-recursive programs
without array operations. First, we generalize ranking functions to the notion
of measure functions, and prove that measure functions (i) provide a sound method
to prove termination of recursive programs (with one-dimensional arrays), and
(ii) is both sound and complete over recursive programs without array operations.
Our second contribution is the synthesis of measure functions of specific forms
in polynomial time. More precisely, we prove that (i) polynomial measure functions
over recursive programs can be synthesized in polynomial time through Farkas’
Lemma and Handelman’s Theorem, and (ii) measure functions involving logarithm
and exponentiation can be synthesized in polynomial time through abstraction of
logarithmic or exponential terms and Handelman’s Theorem. A key application of
our method is the worst-case analysis of recursive programs. While previous methods
obtain worst-case polynomial bounds of the form O(n^k), where k is an integer,
our polynomial time methods can synthesize bounds of the form O(n log n), as well
as O(n^x), where x is not an integer. We show the applicability of our automated
technique to obtain worst-case complexity of classical recursive algorithms such
as (i) Merge-Sort, the divideand-\r\nconquer algorithm for the Closest-Pair problem,
where we obtain O(n log n) worst-case bound, and (ii) Karatsuba’s algorithm for
polynomial multiplication and Strassen’s algorithm for matrix multiplication,
where we obtain O(n^x) bound, where x is not an integer and close to the best-known
bounds for the respective algorithms. Finally, we present experimental results
to demonstrate the\r\neffectiveness of our approach."
alternative_title:
- IST Austria Technical Report
author:
- first_name: '1'
full_name: Anonymous, 1
last_name: Anonymous
- first_name: '2'
full_name: Anonymous, 2
last_name: Anonymous
- first_name: '3'
full_name: Anonymous, 3
last_name: Anonymous
citation:
ama: Anonymous 1, Anonymous 2, Anonymous 3. *Termination and Worst-Case Analysis
of Recursive Programs*. IST Austria; 2016.
apa: Anonymous, 1, Anonymous, 2, & Anonymous, 3. (2016). *Termination and
worst-case analysis of recursive programs*. IST Austria.
chicago: Anonymous, 1, 2 Anonymous, and 3 Anonymous. *Termination and Worst-Case
Analysis of Recursive Programs*. IST Austria, 2016.
ieee: 1 Anonymous, 2 Anonymous, and 3 Anonymous, *Termination and worst-case analysis
of recursive programs*. IST Austria, 2016.
ista: Anonymous 1, Anonymous 2, Anonymous 3. 2016. Termination and worst-case analysis
of recursive programs, IST Austria, 26p.
mla: Anonymous, 1, et al. *Termination and Worst-Case Analysis of Recursive Programs*.
IST Austria, 2016.
short: 1 Anonymous, 2 Anonymous, 3 Anonymous, Termination and Worst-Case Analysis
of Recursive Programs, IST Austria, 2016.
date_created: 2018-12-12T11:39:23Z
date_published: 2016-07-15T00:00:00Z
date_updated: 2020-07-14T23:05:05Z
day: '15'
ddc:
- '000'
file:
- access_level: open_access
checksum: 689069a7abbb34b21516164cbee9e0df
content_type: application/pdf
creator: dernst
date_created: 2019-05-10T13:27:24Z
date_updated: 2020-07-14T12:46:58Z
file_id: '6403'
file_name: popl2017a.pdf
file_size: 686241
relation: main_file
- access_level: closed
checksum: fc08022bfbaac07bac047a9407c0bbb3
content_type: text/plain
creator: dernst
date_created: 2019-05-10T13:27:31Z
date_updated: 2020-07-14T12:46:58Z
file_id: '6404'
file_name: author_names.txt
file_size: 258
relation: main_file
file_date_updated: 2020-07-14T12:46:58Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '26'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '618'
status: public
title: Termination and worst-case analysis of recursive programs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...