Weining Cao

Research Focus: Formal Verification
Current Interest: Formal Verification for Distributed Protocols

📧 Email 🐙 GitHub 📄 Resume

Research Interests

🔍 Formal Verification

🤖 AI for SE

⚙️ Software Engineering

ISSTA 2025
Clause2Inv: A Generate-Combine-Check Framework for Loop Invariant Inference

Weining Cao, Guangyuan Wu, Tangzhi Xu, Yuan Yao, Hengfeng Wei, Taolue Chen, Xiaoxing Ma
📄 View Paper →
ASE 2024
LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference

Guangyuan Wu, Weining Cao, Yuan Yao, Hengfeng Wei, Taolue Chen, Xiaoxing Ma
📄 View Paper →

TLAPS
我们让 Agent 自动写出了 6000 行 TLAPS 证明

Agentic TLAPS proof generation for MongoLoglessDynamicRaft.
📄 Read Blog →