Weining Cao

About

I am a graduate student in the School of Computer Science at Nanjing University and the State Key Laboratory for Novel Software Technology. My research combines large language models with formal reasoning to make verification more automated.

My recent work focuses on inductive invariant inference, counterexample-guided candidate synthesis, and machine-assisted proof development for distributed systems.

Research Interests

Publications

• I3DP · SOSP 2026
  Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models
  Weining Cao, Guangyuan Wu, Yuan Yao, Hengfeng Wei, Taolue Chen, Xiaoxing Ma
  Accepted at SOSP 2026 · First author
  📄 View Preprint → 💻 View Code →
• 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
  First author
  📄 View Paper → 💻 View Code →
• ASE 2024
  LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference
  Guangyuan Wu, Weining Cao, Yuan Yao, Hengfeng Wei, Taolue Chen, Xiaoxing Ma
  Second author · Distinguished Paper Award
  📄 View Paper → 💻 View Code →

Technical Blog

• TLAPS
  How We Used Agents to Produce a 6,000-Line TLAPS Proof
  Agentic TLAPS proof generation for MongoLoglessDynamicRaft.
  📄 Read Blog →

Education & Honors

• EDUCATION
  Nanjing University
  Combined M.S.-Ph.D. program in Computer Science, School of Computer Science and State Key Laboratory for Novel Software Technology, Sep. 2023 - present.
  B.Sc. in Computer Science, Kuang Yaming Honors School, Sep. 2019 - Jun. 2023.
• HONOR
  Distinguished Paper Award, ASE 2024