hide
Free keywords:
-
Abstract:
In an earlier work with Neil D.~Jones, we proposed the ``size-change
principle'' for program termination: An infinite computation is
\emph{impossible}, if it would imply that some data decrease in size
infinitely. Such a property can be deduced from program analysis information in
the form of \emph{size-change graphs}. A set of size-change graphs with the
desired property is said to satisfy \emph{size-change termination} (SCT). There
are many examples of practical programs whose termination can be verified by
creating size-change graphs and testing them for SCT.
While SCT is decidable, it has high worst-case complexity (complete for
\sctext{pspace}). In this paper, we formulate an efficient approach to verify
practical instances of SCT. Our procedure has worst-case complexity cubic in
the input size.
Its effectiveness is demonstrated empirically using a test-suite of over 90
programs.
