## The Polyranking Principle

*
Aaron R. Bradley,
Zohar Manna,
Henny Sipma
*
Although every terminating loop has a ranking function, not every loop
has a ranking function of a restricted form, such as a lexicographic
tuple of polynomials over program variables. The \emph{polyranking
principle} is proposed as a generalization of polynomial ranking for
analyzing termination of loops. We define *lexicographic
polyranking functions* in the context of loops with parallel
transitions consisting of polynomial assertions, including
inequalities, over primed and unprimed variables. Next, we address
*synthesis* of these functions with a complete and automatic
method for synthesizing *lexicographic linear polyranking
functions* with supporting linear invariants over loops in which all
assertions are linear.

In *Proc. 32nd International Colloquium on Automata,
Languages and Programming*, Lisboa, Portugal, July 2005,
Springer Verlag, LNCS 3580, pp 1349-1361.

BibTex,
Postscript,
PDF.
© 2005, Springer Verlag.

© Henny Sipma /
sipma@cs.stanford.edu
Last modified: Wed Mar 28 16:10:48 PST 2001