QCP: A Practical Separation Logic-Based C Program Verification Tool
本文系统介绍 Qualified C Programming Verifier：一个基于分离逻辑、面向实际 C 程序的验证工具。QCP 通过易读的标注语言、符号执行、可定制策略和自动求解，兼顾交互体验、证明自动化与可信性。
Publications
QCP 源于扎实的程序验证研究。本页汇总团队在程序验证、系统及相关方向的论文成果。
9
篇论文
QCP 工具论文
2026
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, and Qinxiang Cao
SL-VC: A Benchmark and Automated Framework for Separation Logic Verification Condition Proving
Hanyang Wang, Xiwei Wu, and Qinxiang Cao
MALICE: Memory-aware Loop Invariants Generation on Symbolic Execution Traces
Tong Chen, Siyu Liu, Hongyi Zhong, Liao Zhang, Lixiang Wang, Xiwei Wu, Junchi Yan, and Qinxiang Cao
Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs (Functional Pearl)
Shushu Wu, Chengxi Yang, Xiwei Wu, and Qinxiang Cao
Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel
Tianqi Zhao, Qinxiang Cao, Shenghua Feng, Minghui Zhou, Naijun Zhan, Yongzhi Cao, Junfeng Zhao, Haiyan Zhao, Hao Wang, and Zhenjiang Hu
Intuitive Verification of Sequential Programs Using Hybrid Reasoning
Shushu Wu, Xiwei Wu, Chengxi Yang, and Qinxiang Cao
2025
VEP: A Two-stage Verification Toolchain for Full eBPF Programmability
Xiwei Wu, Yueyang Feng, Tianyi Huang, Xiaoyang Lu, Shengkai Lin, Lihan Xie, Shizhen Zhao, and Qinxiang Cao
Encode the ∀∃ Relational Hoare Logic into Standard Hoare Logic
Shushu Wu, Xiwei Wu, and Qinxiang Cao
2024
Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation
Chang Liu, Xiwei Wu, Yuan Feng, Qinxiang Cao, and Junchi Yan