Publications

• Certified Program Synthesis with a Multi-Modal Verifier
  Yueyang Feng^*, Dipesh Kafle^*, Vladimir Gladshtein, Vitaly Kurin, George Pîrlea, Qiyuan Zhao, Peter Müller, Ilya Sergey
  41st IEEE/ACM International Conference on Automated Software Engineering (ASE 2026), to appear.
  ^*These authors contributed equally to this work.

• Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean
  Vladimir Gladshtein, Vitaly Kurin, Yueyang Feng, Dipesh Kafle, George Pîrlea, Qiyuan Zhao, Ilya Sergey
  38th International Conference on Computer Aided Verification (CAV 2026), pp. 228–242.
  Distinguished Paper Award

• QCP: A Practical Separation Logic-Based C Program Verification Tool
  Xiwei Wu, Yueyang Feng^*, Xiaoyang Lu^*, Tianchuan Lin, Kan Liu, Zhiyi Wang, Shushu Wu, Lihan Xie, Chengxi Yang, Hongyi Zhong, Zihan Zhang, Juanru Li, Naijun Zhan, Zhenjiang Hu, Qinxiang Cao^†
  20th International Symposium on Theoretical Aspects of Software Engineering (TASE 2026), pp. 157–173.
  ^*These authors contributed equally to this work.
  ^†Corresponding author.

• A Complete Program Logic for Compositional Linearizability
  Eashan Hatti, Arthur Oliveira Vale, Zhongye Wang, Yueyang Feng, Zhong Shao
  40th European Conference on Object-Oriented Programming (ECOOP 2026), Article 11, pp. 11:1–11:28.
  Distinguished Paper Award

• VEP: A Two-stage Verification Toolchain for Full eBPF Programmability
  Xiwei Wu, Yueyang Feng^*, Tianyi Huang^*, Xiaoyang Lu^*, Shengkai Lin, Lihan Xie, Shizhen Zhao^†, Qinxiang Cao^†
  22nd USENIX Symposium on Networked Systems Design and Implementation (NSDI 2025), pp. 277–299.
  ^*These authors contributed equally to this work.
  ^†Corresponding authors.