Modeling and Verification of CKB Consensus Protocol in Coq. - Xiaokun Luan; Meng Sun 002 (QRS Companion, 2021)

Using LSTM to Predict Tactics in Coq. - Xiaokun Luan; Xiyue Zhang 001; Meng Sun 002 (SEKE, 2021)

MedTiny: Enhanced Mediator Modeling Language for Scalable Parallel Algorithms. - Xiangyu Li; Yihao Zhang; Xiaokun Luan; Xiaoyong Xue; Meng Sun 002 (QRS Companion, 2023)

HeatC: A Variable-Grained Coverage Criterion for Deep Learning Systems. - Weidi Sun; Yuteng Lu; Xiaokun Luan; Meng Sun 002 (SETTA, 2023)

Towards Large Language Model Aided Program Refinement. - Yufan Cai; Zhe Hou; Xiaokun Luan; David Sanán; Yun Lin 001; Jun Sun 001; Jin Song Dong (CoRR, 2024)

Protecting Deep Learning Model Copyrights with Adversarial Example-Free Reuse Detection. - Xiaokun Luan; Xiyue Zhang 001; Jingyi Wang 004; Meng Sun 002 (CoRR, 2024)

The Fusion of Large Language Models and Formal Methods for Trustworthy AI Agents: A Roadmap. - Yedi Zhang; Yufan Cai; Xinyue Zuo; Xiaokun Luan; Kailong Wang 001; Zhe Hou; Yifan Zhang; Zhiyuan Wei; Meng Sun 002; Jun Sun 001; Jing Sun 002; Jin Song Dong (CoRR, 2024)

MedTiny Code Generation for Enhancing RegLang Smart Contract Reliability. - Xiaokun Luan; Yihao Zhang; Meng Sun 002 (SAC, 2025)

Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus. - Yufan Cai; Zhe Hou; David Sanán; Xiaokun Luan; Yun Lin 001; Jun Sun 001; Jin Song Dong (Proc. ACM Program. Lang., 2025)

Generically Automating Separation Logic by Functors, Homomorphisms, and Modules. - Qiyuan Xu; David Sanán; Zhe Hou; Xiaokun Luan; Conrad Watt; Yang Liu 003 (Proc. ACM Program. Lang., 2025)

Why the Proof Fails in Different Versions of Theorem Provers: An Empirical Study of Compatibility Issues in Isabelle. - Xiaokun Luan; David Sanán; Zhe Hou; Qiyuan Xu; Chengwei Liu; Yufan Cai; Yang Liu 003; Meng Sun 002 (Proc. ACM Softw. Eng., 2025)

Robust and Efficient Watermarking of Large Language Models Using Error Correction Codes. - Xiaokun Luan; Zeming Wei; Yihao Zhang; Meng Sun 002 (Proc. Priv. Enhancing Technol., 2025)

Psychometric-Based Evaluation for Theorem Proving with Large Language Models. - Jianyu Zhang; Yongwang Zhao; Long Zhang; Jilin Hu; Xiaokun Luan; Zhiwei Xu; Feng Yang (CoRR, 2025)