Biting Huang

Biting Huang

Ph.D. student at Tsinghua University, focusing on formal verification.

Publications

You can also find my articles on my Google Scholar profile.

Conference Papers

LLM-Guided Loop Bound Generation for Program Termination Verification

Published in the 43rd International Conference on Machine Learning (ICML’26), 2026

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.

Accurate Inference of Termination Conditions

Published in IEEE/ACM 48th International Conference on Software Engineering (ICSE’26), 2026

We present the first approach to infer accurate termination conditions of programs. It builds on a simple but effective framework where non-terminating states are iteratively identified and removed, and a termination prover is employed to validate the current condition. We instantiate the framework with data-driven provers and design a multi-way data sharing mechanism to enhance their interaction. Our proofs show that this method is correct, accurate, terminating, and relatively complete. Additionally, we introduce generalization techniques for recurrent sets to accelerate the iteration process. Evaluation on a benchmark of programs from the literature shows that our implementation significantly outperforms the state-of-the-art tool Acabar, producing much more accurate termination conditions, with the proposed techniques playing a crucial role in speeding up the convergence of the process.