Rainfall system uses llms to prove loop termination automatically
Ranking Function Generation with LLMs for Termination
Software EngineeringArtificial IntelligenceLogic in Computer Science
Summary
Loops in computer programs sometimes run forever, which can cause software to get stuck. One way to prove loops do finish is by creating ranking functions, but doing this by hand is very hard. The authors propose RAINFALL, a system that uses large language models (LLMs) combined with symbolic verification to automatically find these ranking functions. When the system’s answer is wrong, it gets feedback from a checker and tries again until it succeeds. This approach works well on many test programs, outperforming previous tools.
What this means in practice
- •For software verification engineers: Automatically generate proofs that loops in C code always finish to improve software reliability checks.
- •For program analysis tool developers: Integrate LLM-guided synthesis of ranking functions to boost the success rate of termination verification tools.
Authors
Rongkang Li, Jiaxin Hu, Taolue Chen, Yong Li, Fu Song, Zhilin Wu
Abstract
Ranking functions are a fundamental technique for proving loop termination, but constructing them manually is challenging and requires substantial expertise. We propose RAINFALL, a neuro-symbolic framework which follows the generate-verify-refine paradigm and tightly integrates LLMs with symbolic verification. RAINFALL formulates ranking function synthesis as a code-completion task by inserting placeholders into the input program and constraining the LLM to fill four predefined slots for each loop. The completed program is then checked by a symbolic verifier. If verification succeeds, a valid ranking function is obtained; otherwise, the verifier's diagnostics are translated into natural-language feedback that guides iterative refinement of the LLM's output. We evaluate RAINFALL on two public benchmark suites comprising 358 terminating C programs. Using MiniMax V2.7, RAINFALL synthesizes verifiable ranking functions for 323 programs (90.22%), outperforming all promising baselines. In particular, it solves 12 more programs than PROTON 2.1, the best-performing baseline and winner of the SV-COMP 2026 Termination category. Furthermore, combining RAINFALL with PROTON 2.1 increases the success rate to 96.65% (346/358 programs). We also conduct ablation study confirming individual contributions of placeholder contracts, few-shot examples, symbolic verification, and diagnostic information feedback. Experiments across LLMs further confirm the effectiveness of RAINFALL. Our results suggest a generic, sound framework for ranking-function synthesis and, beyond termination, LLM-assisted synthesis of formally checkable liveness certificates, both of which represent new directions of software engineering research.