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.

翻译：随着软件系统规模和复杂性的急剧增长，确保其正确性、安全性和可靠性成为日益严峻的挑战。尽管验证技术和工具取得了显著进展，但在自动化能力和表达能力方面的关键缺口，往往阻碍了它们在复杂真实系统中的实际应用。为解决这些困难，本文提出了一种新颖的验证工具——**合格C编程验证器（QCP）**，该工具将基于注解的自动验证与使用Rocq的交互式证明相结合。QCP采用符号执行和分离逻辑蕴含求解器来自动处理大量验证义务，同时将更复杂的验证义务交给Rocq进行手动证明。此外，QCP还包含一款旨在提升证明效率、支持更深入理解程序行为与验证结果的VS Code扩展。