QCP: A Practical Separation Logic-based C Program Verification Tool
Abstract
As software systems increase in size and complexity dramatically, ensuring their correctness, security, and reliability becomes an increasingly formidable challenge. Despite significant advancements in verification techniques and tools, their practical application to complex, real-world systems is often hindered by critical gaps in both automation and expressiveness. To address these difficulties, this paper presents \textbf{Qualified C Programming Verifier (QCP)}, a novel verification tool that integrates annotation-based automatic verification with interactive proving using Rocq. QCP employs symbolic execution and a separation logic entailment solver to automatically discharge many verification obligations, while deferring more complex obligations to Rocq for manual proof. Furthermore, QCP includes a VS Code extension designed to enhance proof efficiency and support a deeper understanding of both the program behavior and verification outcomes.
Cite
@article{arxiv.2505.12878,
title = {QCP: A Practical Separation Logic-based C Program Verification Tool},
author = {Xiwei Wu and Yueyang Feng and Xiaoyang Lu and Tianchuan Lin and Kan Liu and Zhiyi Wang and Shushu Wu and Lihan Xie and Chengxi Yang and Hongyi Zhong and Zihan Zhang and Juanru Li and Naijun Zhan and Zhenjiang Hu and Qinxiang Cao},
journal= {arXiv preprint arXiv:2505.12878},
year = {2026}
}