@InProceedings{leejonesbenamram01,
  AUTHOR       = {Lee, Chin Soon and Jones, Neil D. and Ben-Amram, Amir M.},
  YEAR         = {2001},
  TITLE        = {The Size-Change Principle for Program Termination},
  BOOKTITLE    = POPL,
  editor       = {},
  publisher    = {ACM press},
  organization = {},
  address      = {},
  series       = {},
  volume       = {28},
  pages        = {81--92},
  month        = {january},
  keywords     = {termination, program analysis, lexical order, pspace
hardness},
  summary = {The ``size-change termination''  principle for a first-order
functional language with well-founded data is: a program terminates on all
inputs if every infinite call sequence (following program control flow)
would cause an infinite descent in some data values.
Size-change analysis is based only on local
approximations to parameter size changes derivable from program syntax.
We show how the criterion can be decided using tools from automata theory,
as well as with a direct algorithm operating on ``size-change graphs''.
We establish the  problem's intrinsic complexity to be complete for PSPACE.
The approach is also compared to other termination analyses in the literature.}
  PUF          = {Artikel i proceedings (med censur)},
  POSTSCRIPT   = {http://www.diku.dk/~neil/term.ps}
 }