  Detecting non-termination is crucial for ensuring program correctness and
security, such as preventing denial-of-service attacks. While termination
analysis has been studied for many years, existing methods have limited
scalability and are only effective on small programs. To address this issue, we
propose a practical termination checking technique, called EndWatch, for
detecting non-termination caused by infinite loops through testing.
Specifically, we introduce two methods to generate non-termination oracles
based on checking state revisits, i.e., if the program returns to a previously
visited state at the same program location, it does not terminate. The
non-termination oracles can be incorporated into testing tools (e.g., AFL used
in this paper) to detect non-termination in large programs. For linear loops,
we perform symbolic execution on individual loops to infer State Revisit
Conditions (SRCs) and instrument SRCs into target loops. For non-linear loops,
we instrument target loops for checking concrete state revisits during
execution. We evaluated EndWatch on standard benchmarks with small-sized
programs and real-world projects with large-sized programs. The evaluation
results show that EndWatch is more effective than the state-of-the-art tools on
standard benchmarks (detecting 87% of non-terminating programs while the best
baseline detects only 67%), and useful in detecting non-termination in
real-world projects (detecting 90% of known non-termination CVEs and 4 unknown
bugs).
