Applying this approach to a program involves two steps:
Compared to other approaches to termination analysis, the size-change termination approach is surprisingly simple and general: proofs by lexicographic orders, multiset descent, descent of the maximum or minimum among a set of variables, and other scenarios are all handled automatically and without special treatment, with no need for synthesizing orderings on program states. Another aspect of its generality is that the approach is applicable to all kinds of programs: functional programs (even high-order), imperative programs, logic programs. All these cases can be found in the bibliography. In fact, it is a benefit of the modularity of the approach that only the "front end" needs to be adapted to a programming language. This could allow for "back end" software to be shared, although there are still technical challenges on the road to fully exploiting this opportunity.
Here are slides from an overview
talk about size-change termination. The overview also touches on the more recent extensions described below.
For more advanced students of the topic,
perhaps these
slides from some lectures I gave might also be useful.
Generally, a CTS is a directed graph, which may be understood as the control-flow graph of the program, and whose arcs represent state transitions. A state is described by the control-flow point (node in the graph) plus a finite number of state variables. Every arc is annotated with a formula that specifies constraints on the state variables before and after the transition. Thus, depending on the domain of the variables and the expressivity of the constraint language, a CTS may be as expressive as a concrete program (for example, using natural numbers and a rather simple constraint language, we can represent a counter automaton). We may write CTS(L,D) for Constraint Transition Systems using the constraint language L over data D. The original SCT abstraction is CTS(scg,Ord) where scg stands for size-change graphs and Ord for well-founded sets. Recently, I have been working with CTS(mc,Int), the language of monotonicity constraints over the integers. Monotonicity constraints generalize size-change graphs as they are arbitrary conjunctions of relations of the kinds "greater than" or "greater than or equal to" between any pair of variables in the source and target states.
CTSs over the integers are suitable for representation of a wide range of programs (and the programs where SCT has been found useful typically use the natural numbers as the well-founded domain and therefore can also be represnted in CTS(mc,Int)). Research has established that a lot of the good understanding we have for the SCT abstraction can be extended to this more expressive model. For details look for related publications below.
(in chronological order)
The Size-Change Principle for Program Termination (with C. S. Lee and N. D. Jones), POPL 2001:
General Size-Change Termination and Lexicographic Descent,
LNCS Vol. 2566, 2002:
A paper relating size-change termination with lexicographic descent,
proving that while size-change termination encompasses rich class
of programs, in terms of computability this class is not stronger then
the class of programs with termination governed by lexicographic descent.
This affirmed a conjecture previously made by Neil Jones.
Note that the result has now become a corollary of later
results on ranking functions, see below.
Size-Change Termination in Polynomial Time
(with C. S. Lee), ACM TOPLAS, 29:1 (2007):
This is research on how to perform the SCT analysis phase (the second
step) efficiently. We propose a polynomial-time
algorithm which we have also implemented. We claim that while the
algorithm cannot recognize every terminating instance (as you might
expect, given its efficiency), it covers a range of dataflow patterns
that is sufficiently rich for wide applicability.
Size-Change Termination with Difference Constraints
ACM TOPLAS, 30:3 (2008):
This is research on how to deduce size-change termination when bounds on
increases are also pertinent (e.g., something increases and than
decreases even more). As in the LJB paper, an abstract
formulation of the problem and a theoretical complexity analysis is
presented.
A Complexity Tradeoff in Ranking-Function Termination Proofs
Acta Informatica 46:1 (2009):
Codish, Lagoon and Stuckey (ICLP 2005) noted an intimate relation of
SCT termination proofs to proofs based on local, linear
ranking functions (these concepts are taken from previous work but
definitions are given in the paper).
It's the locality that allows for the ranking
functions to have a simple form (global ranking functions for SCT programs
may be quite complex). But then, in the local approach,
many ranking functions may be needed. This paper proves (under
various sets of assumptions) that such a tradeoff is inherent.
A SAT-Based Approach to Size Change Termination with Global Ranking Functions
(with Mike Codish), TACAS 2008:
We present a class of ranking functions which is strong enough for
supplying termination witnesses for a significant subset of SCT instances.
The subset of SCT instances covered is an NP-complete set.
We have implemented an algorithm that recognizes these instances, using a SAT
solver, and provides the ranking function: see SCNP in the implementations
section below.
Ranking Functions for Size-Change Termination II
(with Chin Soon Lee), Logical Methods in Computer Science Vol.5
Issue 2 (2009):
Improves on the complexity of global ranking functions constructed from SCT instances
from triply-exponential (the upper bound known from the previous paper by CS Lee) to
singly exponential, however for restricted classes of instances. We also prove matching lower
bounds.
Size Change Termination, Monotonicity Constraints
and Ranking Functions
(Logical Methods in Computer Science, Vol.6 Issue 3, 2010):
Considers Monotonicity Constraints, a program
abstraction that extends the SCT abstraction, and carries
the essentials of the theory developed for SCT into this
extended framework. It also
presents an algorithm to construct global ranking functions
for any such program, which also settles the problem of
constructing GRFs for unrestricted SCT instances in singly-exponential complexity. MCs have an advantage of applicability to
the Integer domain, which is not well-founded. The results are extended to
this setting in:
Monotonicity Constraints for Termination in the Integer Domain
(Logical Methods in Computer Science, Vol. 7 (3), 2011.).
SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers
(with Codish, Gonopolskiy, Fuhs and Giesl),
Theory and Practice of Logic Programming, vol. 11, issue 4-5, pp. 503-520, 2011:
We introduce a class of termination witnesses, generalizing lexicographic ranking functions,
designed for Integer Monotonicity Constraint Transition Systems.
The subset of Constraint Transition Systems that has such witnesses is in NP and
we have implemented an algorithm that recognizes these instances, using a SAT
solver. We demonstrated its effectivity on benchmark suites of over 200 CTSs extracted from Java Bytecode programs
by two different front-ends, and a few dozen CTSs from other sources.
Bounded Termination of Monotonicity-Constraint Transition Systems
(with Michal Vainer):
We show that Monotonicity Constraint Transition Systems programs have a decidable complexity property:
one can determine whether the length of all transition sequences can be bounded in terms of the initial state.
We prove that the decision problem is PSPACE-complete. Moreover,
if a bound exists, it must be polynomial. This may imply a complexity result for a source program from
which the MCTS is extracted, depending on the source language and the way it is abstracted.
Ranking Functions for Size-Change Termination: A Practical Procedure to Derive Them by Chin Soon Lee: global ranking-function generation from a set of size-change graphs. A web-demo of an algorithm more sophisticated and in general far more efficient than the one described in my paper.
SCT and SCP implementation by Chin Soon Lee: SCP stands for Size-Change termination in Polynomial time. This implementation accompanies our joint paper listed above. It was meant to compare the polynomial-time algorithm with the precise (graph closure) algorithm. The implementation of the latter is graph-based and somewhat optimized. C code is downloadable. This implementation is a back end; it can read size-change graphs in a simple ascii text format. For a front end, we used Terminweb (see below).
In this paper, James Avery analyzes C programs using a variant of the SCT method. It considers both descending and ascending values, together with information about bounded expressions to replace the well-foundedness assumption. The goal is to handle programs that compute over the integers. (The web site by is currently out of order)
William Blum's MSc Thesis includes an implementation of SCT analysis for a rudimentary high-order functional language. Source code is available.
Ariel's Snir MSc project is a demo implementation of gloabl ranking-function generation from size-change graphs or monotonicity constraints (based on the LMCS 2010 article listed above). To try out the software itself, please contact Amir Ben-Amram.
Termilog is a termination analyzer for Prolog, based on work by Lindenstrauss, Y. Sagiv and others. Terminweb is based on work by Codish, Taboch and others. Both systems include both a program analysis (that determines norms for variables and generates constraints) and a closure analysis (similar to SCT analysis). (The on-line demonstration interface of Terminweb is currently out of order)
SCNP is an SCT subset that has polynomial-size termination witnesses, namely expressions whose value decreases on every transition (ranking functions). This web-accessible analyser takes a size-change graph set and, if it is in SCNP, exhibits the ranking expression. (The web application is currently out of order)
MCNP is an implementation of a SAT-solver-based strategy to termination analysis with monotonicity constraints over the integers. It has been applied with satisfactory success to analyze constraint-transition systems obtained by abstracting imperative programs, mostly in Java; we have a web page with experimental evaluation.
On-line SCT Analyzer by Carl C. Frederiksen: analyzes programs in a simple first-order functional language, creates and graphically displays size-change graphs and performs closure computation and termination deduction. Thus, it includes both a front end (program analysis) component and a back end (termination analysis from size-change graphs, using the graph closure algorithm). (The web application is currently out of order)
PGG is a partial evaluator for Scheme. In this implementation by Arne Glenstrup, SCT analysis (tailored to the needs of a specializer) is used to guarantee termination.
AProVE is a termination checker targeted at term rewriting systems, but also accepting input in several programmer-oriented formalisms, including Haskell syntax. AProVE incorporates the SCT method, as described in the bibliography.
ACL2s includes a programming language (a LISP dialect) and a theorem proving system. Among other features, it now incorporates an automatic termination prover that uses SCT.
The theorem prover Isabelle now uses SCNP (see above) for verifying recursive function definitions.
the Julia termination prover for Java bytecode transforms the JBC program into a CLP (constraint logic program) which is handled by methods which resemble Terminweb above.