On-the-Fly Adapting Code Summarization on Trainable Cost-Effective Language Models. - Yufan Cai 001; Yun Lin 001; Chenyan Liu; Jinglian Wu; Yifan Zhang; Yiming Liu; Yeyun Gong; Jin Song Dong 001 (NeurIPS, 2023)

CoEdPilot: Recommending Code Edits with Learned Prior Edit Relevance, Project-wise Awareness, and Interactive Nature. - Chenyan Liu; Yufan Cai 001; Yun Lin 001; Yuhuan Huang; Yunrui Pei; Bo Jiang; Ping Yang; Jin Song Dong 001; Hong Mei 001 (ISSTA, 2024)

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

The Fusion of Large Language Models and Formal Methods for Trustworthy AI Agents: A Roadmap. - Yedi Zhang; Yufan Cai 001; 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 001 (CoRR, 2024)

Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus. - Yufan Cai 001; Zhe Hou; David Sanán; Xiaokun Luan; Yun Lin 001; Jun Sun 001; Jin Song Dong 001 (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 001; Yang Liu 003; Meng Sun 002 (Proc. ACM Softw. Eng., 2025)

PAT-Agent: Autoformalization for Model Checking. - Xinyue Zuo; Yifan Zhang; Hongshu Wang; Yufan Cai 001; Zhe Hou; Jing Sun 002; Jin Song Dong 001 (CoRR, 2025)