LLM-Guided Loop Bound Generation for Program Termination Verification

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.

Computer programs sometimes enter loops, repeatedly running the same code; if such a loop never stops, the program can hang or waste resources. Proving in advance that a loop will always stop is a hard problem. We introduce LIFT, a system that uses large language models to help with this proof task. Instead of asking the model to write a fragile full mathematical proof, LIFT asks it to suggest a safe upper estimate of how many times a loop can run. A formal checker then tests each suggestion, so LIFT only reports a program as terminating when the check succeeds. When a suggestion is too small/invalid, or hard to check, LIFT analyzes the failure and gives the language model targeted feedback before asking it to try again. This lets LIFT combine the pattern-finding and code-understanding strengths of language models with the reliability of traditional verification tools. On 171 public benchmark programs, LIFT proves 152 programs terminating, outperforming the existing AI-based and conventional tools evaluated in the paper.