Venue: OOPSLA, 2026
A proof language specially designed for reducing and normalizing the notions that have to be learned by LLMs, therefore improving LLMs’ capability
Authors: Qiyuan Xu, Renxi Wang, Peixin Wang, Haonan Li, Conrad Watt
Download Paper | Download Bibtex
Venue: ICLR, 2026
A benchmark aimed at applying Neural Theorem Proving to VC proving, a key bottleneck in the program verification industry
Authors: Qiyuan Xu, Xiaokun Luan, Renxi Wang, Joshua Ong Jun Leang, Peixin Wang, Haonan Li, Wenda Li, Conrad Watt
Download Paper | Download Bibtex
Venue: FSE, 2025
A software engineering work for proof repair over Isabelle.
Authors: Xiaokun Luan, David Sanan, Zhe Hou, Qiyuan Xu, Chengwei Liu, Yufan Cai, Meng Sun
Download Paper | Download Bibtex
Venue: POPL, 2025
Several generic abstract algebras for Separation Logic predicates are found, above which generic automations are built to reason about data structures and algorithms
Authors: Qiyuan Xu, David Sanan, Zhe Hou, Xiaokun Luan, Conrad Watt, Yang Liu
Download Paper | Download Slides | Download Bibtex