We present a technique to prove termination of multipath polynomial programs, an expressive class of loops that enables practical code abstraction and analysis. The technique is based on finite differences of expressions over transition systems. Although no complete method exists for determining termination for this class of loops, we show that our technique is useful in practice. We demonstrate that our prototype implementation for C source code readily scales to large software projects, proving termination for a high percentage of targeted loops.
In Proc.of Verification, Model Checking and Abstract Interpretation (VMCAI'05), LNCS 3385, Springer Verlag, 2005.
BibTex, Postscript, PDF. © 2005, Springer Verlag.