QCP: A Practical Separation Logic-based C Program Verification Tool
For developers and researchers needing to verify complex C programs, QCP offers a hybrid approach that balances automation and expressiveness, though it is an incremental tool combining existing techniques.
QCP integrates automatic annotation-based verification with interactive proving in Rocq to verify C programs, using symbolic execution and a separation logic entailment solver for automation and a VS Code extension for proof efficiency. No concrete performance numbers are provided.
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.