Date Added: Sep 2009
When a running program becomes unresponsive, it is often impossible for a user to determine if the program is performing some useful computation or if it has entered an infinite loop. The authors present LOOPER, an automated technique for dynamically analyzing a running program to prove that it is non-terminating. LOOPER uses symbolic execution to produce simple non-termination arguments for infinite loops dependent on both program values and the shape of heap. The constructed arguments are verified with an off-the-shelf SMT solver. They have implemented their technique in a prototype tool for Java applications, and they demonstrate their technique's effectiveness on several non-terminating benchmarks, including a reported infinite loop bug in open-source text editor jEdit.