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).

翻译：检测非终止问题对于确保程序正确性和安全性（例如防止拒绝服务攻击）至关重要。尽管终止分析已研究多年，但现有方法可扩展性有限，仅对小规模程序有效。为解决此问题，我们提出一种实用的终止检查技术"EndWatch"，通过测试检测由无限循环导致的非终止行为。具体而言，我们引入两种基于状态复访检查生成非终止预言的方法：若程序在同一程序位置返回先前访问过的状态，则表明其不会终止。该非终止预言可集成到测试工具（如本文使用的AFL）中，用于检测大规模程序中的非终止问题。对于线性循环，我们通过对单个循环执行符号执行推断状态复访条件（SRCs），并将SRC注入目标循环；对于非线性循环，我们在目标循环中注入检测代码，用于在运行时检查具体状态复访。我们在包含小规模程序的标准基准测试集和包含大规模程序的真实项目上评估了EndWatch。评估结果表明，EndWatch在标准基准测试上优于现有最先进工具（检测87%的非终止程序，而最佳基线仅检测67%），并能有效检测真实项目中的非终止问题（检测到90%已知非终止CVE漏洞及4个未知缺陷）。