Termination of Polynomial Programs

We present a technique to prove termination of multipath polynomial programs, an expressive class of loops that enables practical traction 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.

• Type: Conference
• Year: 2005
• Where: VMCAI
• Authors: Aaron R. Bradley, Zohar Manna, Henny B. Sipma
• Keywords: Complete Method Exists, Expressive Class, Multipath Polynomial Programs, Software Engineering, VMCAI 2005