Detecting Infinite Loops


Checking software termination is, in general, undecidable, but has been shown decidable for certain classes of programs. In particular, termination checking for loops with linear assignments is decidable. This project aims to create an extension for Java Pathfinder which can determine whether non-terminating loops of this form are present in a given program.


student: Kevin Durant

mentor: Willem Visser



The sources for this project will be made available through the jpf-symbc project.


We have implemented an algorithm to discover infinite paths through while loop programs in which the variables in the loop condition are only transformed with affine functions. The infinite paths gathered in this manner are repetitive, that is, after a fixed number of iterations the loop condition is no nearer to being violated than it was initially. We have a proof showing that this period of repetition is 2 for the one variable case, while for the two variable case simulations suggest that the maximum period is at least 6, but a fixed period is not yet known. The algorithm is implemented as a listener in Symbolic PathFinder. A paper describing the work has appeared at the JPF 2011 workshop.

Last modified 6 years ago Last modified on 03/11/2012 09:23:39 PM