Anonymous, 1 and Anonymous, 2 and Anonymous, 3 (2016) Termination and WorstCase Analysis of Recursive Programs. Technical Report. Anonymous. (Submitted)
Text
popl2017a.pdf  Submitted Version Restricted to Registered users only Available under License All rights reserved. [IST2016618v1+1] Download (539Kb) 

Text
listofauthors1.txt  Additional Metadata Restricted to Repository staff only [IST2016618v1+2] Download (258b) 
Abstract
We study the problem of developing efficient approaches for proving termination of recursive programs with onedimensional arrays. Ranking functions serve as a sound and complete approach for proving termination of nonrecursive 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 onedimensional 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 worstcase analysis of recursive programs. While previous methods obtain worstcase 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 worstcase complexity of classical recursive algorithms such as (i) MergeSort, the divideand conquer algorithm for the ClosestPair problem, where we obtain O(n log n) worstcase 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 bestknown bounds for the respective algorithms. Finally, we present experimental results to demonstrate the effectiveness of our approach.
Item Type:  Monograph (Technical Report) 

Subjects:  000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems > 005 Computer programming, programs & data 000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems > 006 Special computer methods 
Depositing User:  Anonymous User 
Date Deposited:  15 Jul 2016 09:07 
Last Modified:  15 Jul 2019 14:42 
URI:  https://repository.ist.ac.at/id/eprint/618 
Actions (login required)
View Item 