publications

2026

1. Preprint

   

   VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation

   Zichen Xie, Mrigank Pawagi, Yuxin Liu, and 5 more authors

   arXiv preprint arXiv:2605.08553, 2026

   Bib HTML

   @article{xie2026vericontest,
     title = {VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation},
     author = {Xie, Zichen and Pawagi, Mrigank and Liu, Yuxin and Rai, Aaditi and Shao, Lize and Berberian Jr, John and Che, Sicong and Wang, Wenxi},
     journal = {arXiv preprint arXiv:2605.08553},
     year = {2026},
   }

2. ICML 2026

   

   Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought

   Zichen Xie, and Wenxi Wang

   arXiv preprint arXiv:2603.18334, 2026

   Bib HTML

   @article{xie2026can,
     title = {Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought},
     author = {Xie, Zichen and Wang, Wenxi},
     journal = {arXiv preprint arXiv:2603.18334},
     year = {2026},
   }

2025

1. SOSP 2025

   

   Knighter: Transforming static analysis with llm-synthesized checkers

   Chenyuan Yang, Zijie Zhao, Zichen Xie, and 2 more authors

   In Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles, 2025

   Bib HTML

   @inproceedings{yang2025knighter,
     title = {Knighter: Transforming static analysis with llm-synthesized checkers},
     author = {Yang, Chenyuan and Zhao, Zijie and Xie, Zichen and Li, Haoyu and Zhang, Lingming},
     booktitle = {Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles},
     pages = {655--669},
     year = {2025},
   }

2. ISSTA 2025

   

   Beyond Static Pattern Matching? Rethinking Automatic Cryptographic API Misuse Detection in the Era of LLMs

   Yifan Xia, Zichen Xie, Peiyu Liu, and 4 more authors

   Proceedings of the ACM on Software Engineering, 2025

   Abs Bib HTML

   While the automated detection of cryptographic API misuses has progressed significantly, its precision diminishes for intricate targets due to the reliance on manually defined patterns. Large Language Models (LLMs) offer a promising context-aware understanding to address this shortcoming, yet the stochastic nature and the hallucination issue pose challenges to their applications in precise security analysis. This paper presents the first systematic study to explore LLMs’ application in cryptographic API misuse detection. Our findings are noteworthy: The instability of directly applying LLMs results in over half of the initial reports being false positives. Despite this, the reliability of LLM-based detection could be significantly enhanced by aligning detection scopes with realistic scenarios and employing a novel code & analysis validation technique, achieving a nearly 90% detection recall. This improvement substantially surpasses traditional methods and leads to the discovery of previously unknown vulnerabilities in established benchmarks. Nevertheless, we identify recurring failure patterns that illustrate current LLMs’ blind spots. Leveraging these findings, we deploy an LLM-based detection system and uncover 63 new vulnerabilities (47 confirmed, 7 already fixed) in open-source Java and Python repositories, including prominent projects like Apache.

   @article{xia2025beyond,
     title = {Beyond Static Pattern Matching? Rethinking Automatic Cryptographic API Misuse Detection in the Era of LLMs},
     author = {Xia, Yifan and Xie, Zichen and Liu, Peiyu and Lu, Kangjie and Liu, Yan and Wang, Wenhai and Ji, Shouling},
     journal = {Proceedings of the ACM on Software Engineering},
     volume = {2},
     number = {ISSTA},
     pages = {113--136},
     year = {2025},
     publisher = {ACM New York, NY, USA},
   }