Biting Huang

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…