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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Bradley, A. R., Manna, Z., & Sipma, H. B. (2005). Termination of polynomial programs. In Lecture Notes in Computer Science (Vol. 3385, pp. 113–129). Springer Verlag. https://doi.org/10.1007/978-3-540-30579-8_8
Mendeley helps you to discover research relevant for your work.