# Termination and worst-case analysis of recursive programs

Anonymous 1, Anonymous 2, Anonymous 3. 2016. Termination and worst-case analysis of recursive programs, IST Austria, 26p.

Download

*Technical Report*|

*Published*|

*English*

Author

Anonymous, 1;
Anonymous, 2;
Anonymous, 3

Series Title

IST Austria Technical Report

Abstract

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-
conquer 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
effectiveness of our approach.

Publishing Year

Date Published

2016-07-15

Page

26

ISSN

IST-REx-ID

### Cite this

Anonymous 1, Anonymous 2, Anonymous 3.

*Termination and Worst-Case Analysis of Recursive Programs*. IST Austria; 2016.Anonymous, 1, Anonymous, 2, & Anonymous, 3. (2016).

*Termination and worst-case analysis of recursive programs*. IST Austria.Anonymous, 1, 2 Anonymous, and 3 Anonymous.

*Termination and Worst-Case Analysis of Recursive Programs*. IST Austria, 2016.1 Anonymous, 2 Anonymous, and 3 Anonymous,

*Termination and worst-case analysis of recursive programs*. IST Austria, 2016.Anonymous, 1, et al.

*Termination and Worst-Case Analysis of Recursive Programs*. IST Austria, 2016.**All files available under the following license(s):**

**Copyright Statement:**

**This Item is protected by copyright and/or related rights.**[...]

**Main File(s)**

File Name

popl2017a.pdf
686.24 KB

Access Level

Open Access

Date Uploaded

2019-05-10

MD5 Checksum

689069a7abbb34b21516164cbee9e0df

File Name

**author_names.txt**258 bytes

Access Level

Closed Access

Date Uploaded

2019-05-10

MD5 Checksum

fc08022bfbaac07bac047a9407c0bbb3