LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference. - Guangyuan Wu; Weining Cao; Yuan Yao 001; Hengfeng Wei; Taolue Chen 001; Xiaoxing Ma (ASE, 2024)

Clause2Inv: A Generate-Combine-Check Framework for Loop Invariant Inference. - Weining Cao; Guangyuan Wu; Tangzhi Xu; Yuan Yao 001; Hengfeng Wei; Taolue Chen 001; Xiaoxing Ma (Proc. ACM Softw. Eng., 2025)