QCP is grounded in rigorous program-verification research. This page gathers peer-reviewed work by the team in verification, systems, and related areas.
This paper presents the Qualified C Programming Verifier, a separation-logic-based tool for practical C verification. QCP combines a readable annotation language, symbolic execution, customizable strategies, and automated solving to balance usability, automation, and trust.
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, and Qinxiang Cao
Hanyang Wang, Xiwei Wu, and Qinxiang Cao
Tong Chen, Siyu Liu, Hongyi Zhong, Liao Zhang, Lixiang Wang, Xiwei Wu, Junchi Yan, and Qinxiang Cao
Shushu Wu, Chengxi Yang, Xiwei Wu, and Qinxiang Cao
Tianqi Zhao, Qinxiang Cao, Shenghua Feng, Minghui Zhou, Naijun Zhan, Yongzhi Cao, Junfeng Zhao, Haiyan Zhao, Hao Wang, and Zhenjiang Hu
Shushu Wu, Xiwei Wu, Chengxi Yang, and Qinxiang Cao
Xiwei Wu, Yueyang Feng, Tianyi Huang, Xiaoyang Lu, Shengkai Lin, Lihan Xie, Shizhen Zhao, and Qinxiang Cao
Shushu Wu, Xiwei Wu, and Qinxiang Cao
Chang Liu, Xiwei Wu, Yuan Feng, Qinxiang Cao, and Junchi Yan