Publications

2026

  • (ICLR’26, CCF-A) Qiyuan Xu, Xiaokun Luan, Renxi Wang, Joshua Ong Jun Leang, Peixin Wang, Haonan Li, Wenda Li, and Conrad Watt. 2026. “Neural Theorem Proving for Verification Conditions: A Real-World Benchmark.” In The Fourteenth International Conference on Learning Representations.
  • (ICSE’26, CCF-A) Xinyi Zheng, Ningke Li, Xiaokun Luan, Kailong Wang, Ling Shi, Meng Sun, and Haoyu Wang. 2026. “Beyond Correctness: Exposing LLM-generated Logical Flaws in Reasoning via Multi-step Automated Theorem Proving.” In Proceedings of the 48th IEEE/ACM International Conference on Software Engineering.
  • (UAI’26, CCF-B) Nianyun Song, Xiaokun Luan, Yu Guo, Rongfang Bie, Meng Sun, and Xiyue Zhang. 2026. “Privacy-Preserving Robustness Verification for Neural Networks.” In Proceedings of the 42nd Conference on Uncertainty in Artificial Intelligence.

2025

  • (FSE’25, CCF-A) Xiaokun Luan, David Sanan, Zhe Hou, Qiyuan Xu, Chengwei Liu, Yufan Cai, Yang Liu, and Meng Sun. 2025. “Why the Proof Fails in Different Versions of Theorem Provers: An Empirical Study of Compatibility Issues in Isabelle.” Proceedings of the ACM on Software Engineering 2, no. FSE (2025): 1499-1521. Award · ACM SIGSOFT Distinguished Paper
  • (ICML’25, CCF-A) Yedi Zhang, Yufan Cai, Xinyue Zuo, Xiaokun Luan, Kailong Wang, Zhe Hou, Yifan Zhang, Zhiyuan Wei, Meng Sun, Jun Sun, Jing Sun, Jin Song Dong. “Position: Trustworthy AI Agents Require the Integration of Large Language Models and Formal Methods.” In Forty-second International Conference on Machine Learning Position Paper Track (2025).
  • (POPL’25, CCF-A) Qiyuan Xu, David Sanan, Zhe Hou, Xiaokun Luan, Conrad Watt, and Yang Liu. 2025. “Generically Automating Separation Logic by Functors, Homomorphisms, and Modules.” Proceedings of the ACM on Programming Languages 9, no. POPL (2025): 1992-2024.
  • (POPL’25, CCF-A) Yufan Cai, Zhe Hou, David Sanan, Xiaokun Luan, Yun Lin, Jun Sun, and Jin Song Dong. 2025. “Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus.” Proceedings of the ACM on Programming Languages 9, no. POPL (2025): 2057-2089.
  • (TNNLS, SCI-Q1, CCF-B) Xiaokun Luan, Xiyue Zhang, Jingyi Wang, and Meng Sun. “Protecting Deep Learning Model Copyrights With Adversarial Example-Free Reuse Detection.” IEEE Transactions on Neural Networks and Learning Systems (2025).
  • (ICFEM’25, CCF-C) Xiaokun Luan, Zeming Wei, Yihao Zhang, and Meng Sun. 2025. “Automata-Based Steering of Large Language Models for Diverse Structured Generation.” In Formal Methods and Software Engineering (ICFEM 2025), LNCS 16229, pp. 22–41. Springer. Award · Best Paper
  • (PETS’25, CCF-C) Xiaokun Luan, Zeming Wei, Yihao Zhang, Meng Sun. “Robust and Efficient Watermarking of Large Language Models Using Error Correction Codes.” Proceedings on Privacy Enhancing Technologies (2025).
  • (SAC’25) Xiaokun Luan, Yihao Zhang, and Meng Sun. 2025. “MedTiny Code Generation for Enhancing RegLang Smart Contract Reliability”. In Proceedings of the 40th ACM/SIGAPP Symposium on Applied Computing, pp. 1666–1673. 2025.

2023

  • (SETTA’23, CCF-C) Weidi Sun, Yuteng Lu, Xiaokun Luan, and Meng Sun. “HeatC: A Variable-Grained Coverage Criterion for Deep Learning Systems.” In International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, pp. 243-261. Singapore: Springer Nature Singapore, 2023.
  • (QRS-C’23) Xiangyu Li, Yihao Zhang, Xiaokun Luan, Xiaoyong Xue, and Meng Sun. “MedTiny: Enhanced Mediator Modeling Language for Scalable Parallel Algorithms.” In 2023 IEEE 23rd International Conference on Software Quality, Reliability, and Security Companion (QRS-C), pp. 451–460. IEEE, 2023.

2021

  • (SEKE’21, CCF-C) Xiaokun Luan, Xiyue Zhang, Meng Sun. “Using LSTM to Predict Tactics in Coq.” In Proceedings of SEKE 2021, pages 132-137. KSI Research Inc. and Knowledge Systems Institute, 2021.
  • (QRS-C’21) Xiaokun Luan and Meng Sun. 2021. “Modeling and Verification of CKB Consensus Protocol in Coq.” In 2021 IEEE 21st International Conference on Software Quality, Reliability and Security Companion (QRS-C), pp. 660–667. IEEE, 2021.