Data-Driven Loop Bound Learning for Termination Analysis

Termination is a fundamental liveness property for program verification. A loop bound is an upper bound of the number of loop iterations for a given program. The existence of a loop bound evidences the termination of the program. This paper employs a reinforced black-box learning approach for termination proving, consisting of a loop bound learner and a validation checker. We present efficient data-driven algorithms for inferring various kinds of loop bounds, including simple loop bounds, conjunctive loop bounds, and lexicographic loop bounds. We also devise an efficient validation checker by integrating a quick bound checking algorithm and a two-way data sharing mechanism. We implemented a prototype tool called ddlTerm. Experiments on publicly accessible benchmarks show that ddlTerm outperforms state-of-the-art termination analysis tools by solving 13-48% more benchmarks and saving 40-77% solving time. CCS CONCEPTS • Software and its engineering → Formal software verification; • Theory of computation → Logic and verification.