Termination Analysis of Programs with Multiphase Control-Flow

TL;DR

This paper explores methods for proving termination of programs with multiphase control-flow by employing multiphase ranking functions and control-flow refinement techniques, including partial evaluation of Constrained Horn Clauses.

Contribution

It introduces theoretical frameworks for multiphase ranking functions and demonstrates how control-flow refinement simplifies termination proofs.

Findings

Theoretical analysis of multiphase ranking functions for various program representations.

Use of control-flow refinement to facilitate termination proofs.

Application of partial evaluation of Constrained Horn Clauses to simplify control-flow.

Abstract

Programs with multiphase control-flow are programs where the execution passes through several (possibly implicit) phases. Proving termination of such programs (or inferring corresponding runtime bounds) is often challenging since it requires reasoning on these phases separately. In this paper we discuss techniques for proving termination of such programs, in particular: (1) using multiphase ranking functions, where we will discuss theoretical aspects of such ranking functions for several kinds of program representations; and (2) using control-flow refinement, in particular partial evaluation of Constrained Horn Clauses, to simplify the control-flow allowing, among other things, to prove termination with simpler ranking functions.