M.Sc Student | Elenbogen Dima |
---|---|

Subject | Proving Mutual Termination of Programs |

Department | Department of Computer Science |

Supervisors | Professor Ofer Strichman |

Professor Shmuel Katz | |

Full Thesis text |

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.