Program Termination Analysis in Polynomial Time

Abstract

Recall the size-change principle for program termination: An infinite computation is impossible, if it would give rise to an infinite sequence of size-decreases for some data values. For an actual analysis, size-change graphs are used to capture the data size changes in possible program state transitions. A graph sequence that respects program control flow is called a multipath. The set of multipaths describe possible state transition sequences. To show that such sequences are finite, it is sufficient that the graphs satisfy size-change termination (SCT): Every infinite multipath has infinite descent, according to the arcs of the graphs. This is an application of the size-change principle.

SCT is decidable, but complete for pspace. In this paper, we explore efficient approximations that are sufficiently precise in practice. For size-change graphs that can loop (i.e., they give rise to an infinite multipath), and that satisfy SCT, it is usual to find amongst them an anchor— some graph whose infinite occurrence in a multipath causes infinite descent. The SCT approximations are based on finding and eliminating anchors, as far as possible. If the remaining graphs cannot loop, then SCT is established.

An efficient method is proposed to find anchors among fan-in free graphs, as such graphs occur commonly in practice. This leads to a worst-case quadratic-time approximation of SCT. An extension of the method handles general graphs and can detect some rather subtle descent. It leads to a worst-case cubic-time approximation of SCT. Experiments confirm the effectiveness and efficiency of the approximations in practice.

This research is supported by DAEDALUS, the RTD project IST-1999-20527 of the IST Programme within the European Union’s Fifth Framework Programme.