## Termination Analysis of Integer Linear Loops

*
Aaron R. Bradley,
Zohar Manna,
Henny Sipma
*
Usually, ranking function synthesis and invariant generation over a
loop with integer variables involves abstracting the loop to have real
variables. Integer division and modulo arithmetic must be soundly
abstracted away so that the analysis over the abstracted loop is sound
for the original loop. Consequently, the analysis loses precision.
In contrast, we introduce a technique for handling loops over integer
variables directly. The resulting analysis is more precise than
previous analyses.

To appear in *Proc. of the 16th International Conference on
Concurrency Theory (CONCUR'05)*, San Francisco, August 2005

Postscript,
PDF,
© 2005, Springer Verlag.

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