LLM-Guided Loop Bound Generation for Program Termination Verification

Zan Gong, Biting Huang, Fei He
Proceedings of the 43rd International Conference on Machine Learning, PMLR 306:35943-35957, 2026.

Abstract

Program termination is a fundamental liveness property in software verification. Proving termination of a given program is a formidable challenge due to the undecidability of the problem. In this paper, we propose LIFT, a termination verification framework that leverages LLMs to generate loop bounds within a guess-and-check workflow. LIFT couples this generation with a sound formal validation procedure that both guarantees all reported terminations and refutes invalid loop bounds via violation analysis. Experiments on publicly accessible termination benchmarks show that LIFT significantly outperforms existing termination verification tools.

Cite this Paper

BibTeX
@InProceedings{pmlr-v306-gong26e, title = {{LLM}-Guided Loop Bound Generation for Program Termination Verification}, author = {Gong, Zan and Huang, Biting and He, Fei}, booktitle = {Proceedings of the 43rd International Conference on Machine Learning}, pages = {35943--35957}, year = {2026}, editor = {Zhang, Tong and Dudik, Miroslav and Jaggi, Martin and Agarwal, Alekh and Li, Sharon and Schuurmans, Dale and Zhu, Jerry and Berkenkamp, Felix and Dong, Hanze and Bietti, Alberto}, volume = {306}, series = {Proceedings of Machine Learning Research}, month = {06--11 Jul}, publisher = {PMLR}, pdf = {https://raw.githubusercontent.com/mlresearch/v306/main/assets/gong26e/gong26e.pdf}, url = {https://proceedings.mlr.press/v306/gong26e.html}, abstract = {Program termination is a fundamental liveness property in software verification. Proving termination of a given program is a formidable challenge due to the undecidability of the problem. In this paper, we propose LIFT, a termination verification framework that leverages LLMs to generate loop bounds within a guess-and-check workflow. LIFT couples this generation with a sound formal validation procedure that both guarantees all reported terminations and refutes invalid loop bounds via violation analysis. Experiments on publicly accessible termination benchmarks show that LIFT significantly outperforms existing termination verification tools.} }
Endnote
%0 Conference Paper %T LLM-Guided Loop Bound Generation for Program Termination Verification %A Zan Gong %A Biting Huang %A Fei He %B Proceedings of the 43rd International Conference on Machine Learning %C Proceedings of Machine Learning Research %D 2026 %E Tong Zhang %E Miroslav Dudik %E Martin Jaggi %E Alekh Agarwal %E Sharon Li %E Dale Schuurmans %E Jerry Zhu %E Felix Berkenkamp %E Hanze Dong %E Alberto Bietti %F pmlr-v306-gong26e %I PMLR %P 35943--35957 %U https://proceedings.mlr.press/v306/gong26e.html %V 306 %X Program termination is a fundamental liveness property in software verification. Proving termination of a given program is a formidable challenge due to the undecidability of the problem. In this paper, we propose LIFT, a termination verification framework that leverages LLMs to generate loop bounds within a guess-and-check workflow. LIFT couples this generation with a sound formal validation procedure that both guarantees all reported terminations and refutes invalid loop bounds via violation analysis. Experiments on publicly accessible termination benchmarks show that LIFT significantly outperforms existing termination verification tools.
APA
Gong, Z., Huang, B. & He, F.. (2026). LLM-Guided Loop Bound Generation for Program Termination Verification. Proceedings of the 43rd International Conference on Machine Learning, in Proceedings of Machine Learning Research 306:35943-35957 Available from https://proceedings.mlr.press/v306/gong26e.html.

Related Material