Template-Guided Loop Invariant Synthesis Driven by Program Comprehension

Automated loop invariant synthesis is crucial for program verification. While template-guided generation brings new opportunities to this field, the lack of sufficient domain knowledge often results in templates with mismatched complexity, leading to high-degree polynomial terms and ineffective searches. Additionally, current utilizations of counterexamples are inadequate, further limiting the effectiveness of the sub-template. Therefore, we propose the Glue method, which combines static analysis with data learning techniques to enhance synthesis efficiency. We develop a k-GCN to predict template complexity and employ Unsat Core analysis to pinpoint conflicts at a finer clause level. Glue outperforms the existing baseline method in experiments on linear benchmarks with a 17 % increase in successful samples, reducing processing time, decreasing the number of counterexamples, and optimizing iteration efficiency. Ablation studies further confirm the critical roles of our analysis in the success of synthesis.