QCP — C Program Verification Tool

Overview

Abstract

QCP is a C program verification tool developed at Shanghai Jiao Tong University, built upon the foundations of VST and VST-A. It accepts annotated C programs as input, performs symbolic execution based on assertion annotations, and generates Coq proof obligations. Users complete the verification by proving the generated Coq goals. Qide is the web-based interface for QCP.

Input

Annotated C

Frontend

Symbolic Execution

Backend

Coq Proofs

Output

Verified Program

Methodology

QCP consists of two core components: a symbolic execution engine implemented in C and a proof backend implemented in Coq. The symbolic execution component features an enriched annotation language supporting complex C program syntax, and employs strategies and an SMT solver for automated assertion resolution, significantly reducing the manual proof burden.

Output Artifacts

The verification pipeline produces four structured output files:

xxx_proof_goal

Complete list of all proof obligations

xxx_proof_auto

Proofs resolved by strategy & SMT solver

xxx_proof_manual

Obligations requiring manual proof

xxx_proof_check

Final verification check file

Publications

NSDI 2025 · Philadelphia, PA, USA

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

arXiv preprint

Team

Principal Investigators

Cao Qinxiang PI

Project Lead

Li Juanru

Co-Investigator

Researchers & Developers

Wu Xiwei

Frontend language, type inference, symbolic execution

Lu Xiaoyang

Frontend language, type inference, symbolic execution

Feng Yueyang

Symbolic execution, soundness proof

Xie Lihan

SMT solver and proof checker

Wang Zhiyi

Strategy development, soundness proof

Wu Shushu

Relational Hoare Logic proof maintenance

Lin Tianchuan

Symbolic execution, soundness proof

Zhong Hongyi

Strategy parser, concurrency examples

Zhang Zihan

QCP web frontend (Qide)

Yang Chengxi

Relational Hoare Logic, VSCode plugin, symbolic execution

Liu Kan

Separation logic library, Relational Hoare Logic

Liu Siyu

Assertion processing and output

Fang Yi

Assertion processing and output

Tao Yichen

Separation logic library

Special thanks to Prof. Zhan Naijun, Prof. Hu Zhenjiang, and Prof. Yu Yu for their guidance on the QCP tool and its applications. We also gratefully acknowledge the contributions of Dong Yibo, Zhou Litao, Qin Jianxing, Wang Zhongye, Tang Yazhou, Chen Yanning, and Liu Hanzhi for their exploratory work during the early stages of the project.