Automated loop invariant inference through learning-guided program structure analysis

Automated loop invariant inference remains a fundamental challenge in formal verification due to the inherently unbounded search space of candidate invariants. Existing approaches either incur substantial computational overhead during invariant synthesis or rely on manually predefined templates, limiting both scalability and automation. Although recent learning-based methods have shown promise, they often fail to fully exploit the rich structural and semantic information embedded within program representations. This paper presents a learning-guided framework for fully automated loop invariant inference based on a systematic analysis of program structure and semantics. The framework performs a joint analysis of syntactic constructs, control-flow structure, and data-dependence relationships to determine invariant structure before instantiation. These complementary representations are embedded and integrated within a learning-based model that identifies structurally and semantically features and infers expressive invariant templates directly from program structure. The inferred templates are instantiated using execution-derived values, yielding constraint systems that are solved and formally validated using a Satisfiability Modulo Theories solver. Experimental evaluation demonstrates that the proposed approach achieves competitive invariant inference performance on challenging benchmarks. By integrating multi-representation program analysis, the framework effectively supports a wide range of loop structures and advances the state of the art in scalable, expressive, and fully automated loop invariant inference.