QCP是由上海交通大学曹钦翔老师实验室在VST, VST-A的基础上进行开发的C程序验证工具。
QCP延续了VST-A的思路，接受一个带标注的C程序为输入，会基于标注断言对C程序进行符号执行，生成待证明的Coq proof。用户只需要证明相关的Coq proof就能够完成对C程序的证明。
QCP项目分为C实现的符号执行部分和Coq实现的后端证明部分。
在符号执行部分，我们实现了更为丰富的标注语言，能够接受更加复杂的C程序语法，并且使用了strategy和SMT solver来进行断言的自动求解，减少了用户的证明工作量。我们将整个证明分别输出为四个文件：
xxx_proof_goal - 所有待证明结论列表xxx_proof_auto - 已经通过strategy和SMT solver自动解决的相关证明xxx_proof_manual - 需要手动完成的相关证明xxx_proof_check - 所有证明都已经完成的检查文件在后端证明部分，我们实现了与VST类似的proof tactics。
Xiwei Wu, Yueyang Feng, Tianyi Huang, Xiaoyang Lu, Shengkai Lin, Lihan Xie, Shizhen Zhao, Qinxiang Cao, "VEP: A Two-stage Verification Toolchain for Full eBPF Programmability" , in NSDI, Philadelphia, PA, USA, April, 2025.
李卷儒 - jarod@sjtu.edu.cn
吴熙炜 - yashen@sjtu.edu.cn
陆潇扬 - luxy1115@sjtu.edu.cn
前端语言、类型推断、符号执行
冯跃洋 - fyyvexoben@sjtu.edu.cn
符号执行、soundness proof
谢立汉 - sheringham@sjtu.edu.cn
SMT solver和proof checker开发和维护
王治奕 - ginwiahzy@gmail.com
strategy开发和维护，相关soundness proof证明
吴姝姝 - ciel77@sjtu.edu.cn
Relational Hoare Logic部分证明维护
林田川 - lintianchuan@foxmail.com
符号执行、soundness proof
钟泓逸 - zhonghongyi1204@sjtu.edu.cn
strategy parser开发和维护、部分并发用例的开发
张子涵 - 1032ghost@gmail.com
QCP网页端开发和维护
杨承羲 - arcadia-y@sjtu.edu.cn
Relational Hoare Logic、VSCode 插件开发、符号执行
分离逻辑基础库、Relational Hoare Logic
刘思雨 - williamliusy@sjtu.edu.cn
断言处理与输出
方屹 - chnfy@stu.pku.edu.cn
断言处理与输出
陶浥尘 - ychtao@umich.edu
分离逻辑基础库
特别感谢詹乃军老师、胡振江老师和郁昱老师对QCP工具及其应用的指导，特别感谢董弈伯、周李韬、秦健行、王中烨、唐亚周、陈彦宁和刘涵之等同学在项目前期探索方面做出的贡献。