Detecting Infinite Loops
by Kevin Durant for The Java Pathfinder Team
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.