Technical Report MSC-2014-11

TR#:MSC-2014-11
Class:MSC
Title: Proving Mutual Termination of Programs
Authors: Dima Elenbogen
Supervisors: Ofer Strichman, Shmuel Katz
PDFMSC-2014-11.pdf
Abstract: Two programs are said to be mutually terminating if they terminate on exactly the same inputs. We suggest inference rules and a proof system for proving mutual termination of a given pair of functions <f, f’> and the respective subprograms that they call under a free context. Given a (possibly partial) mapping between the functions of the two programs, the premise of the rule requires proving that given the same arbitrary input in, f(in) and f'(in) call functions mapped in the mapping with the same arguments. A variant of this proof rule with a weaker premise allows to prove termination of one of the programs if the other is known to terminate for all inputs. In addition, we suggest various techniques for battling the inherent incompleteness of our solution, including a case in which the interface of the two functions is not identical, and a case in which there is partial information about the partial equivalence (the equivalence of their input/output behavior) of the two given functions.

We present an algorithm for decomposing the verification problem of whole programs to that of proving mutual termination of individual functions, based on our suggested inference rules. The reported prototype implementation of this algorithm is the first to deal with the mutual termination problem.

CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2014/MSC/MSC-2014-11), rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the MSC technical reports of 2014
To the main CS technical reports page

Computer science department, Technion
admin