LLM-Based Invariant Generation for Multi-Loop Programs via Forward and Backward Iterative Refinement
Cloud computing infrastructure increasingly relies on cloud services where correctness is critical. Ensuring their correctness requires formal verification techniques grounded in rigorous mathematical reasoning. In practice, formal models of cloud services frequently exhibit multiple loop structures, and verifying such models depends on the ability to automatically generate sufficient and accurate loop invariants. In this paper, we present an LLM-based invariant generation method for multi-loop programs via forward and backward iterative refinement. The approach is built upon the recent generate-combine-check framework. First, we employ a multiloop structure-guided strategy to instruct the LLM to produce clause expressions without logical connectives, which are then combined via counterexample-driven refinement to form candidate invariants. After that, we use a backward iterative refinement mechanism to adjust the invariants in reverse order, that is, from post-condition at the end of the program, to the inter-loop invariants, and finally to the pre-condition at the beginning of the program. We implemented a prototype tool named MultiInvGen. Evaluation results show that, MultiInvGen successfully solves 71 tasks (65.7%) on a benchmark of 108 C programs, significantly outperforming the state-of-the-art LLMbased and Multi-loop invariant generation tool.