About QCP
QCP (Qualified C Programming) is a C program verification tool. Its core functionality allows users to verify that a C program runs safely and behaves as expected under all permitted conditions. When using QCP, users add specification annotations (such as function pre/post-conditions and loop invariants) to their C code. QCP then uses symbolic execution and separation logic reasoning to transform the program's safety and functional correctness verification into a set of Verification Conditions (VCs). For most simple VCs, QCP uses its built-in solver to complete verification. For parts that cannot be automatically solved, QCP generates Rocq (formerly Coq) proof files, allowing users to manually complete proofs in a theorem prover.
Unlike traditional program verification tools, QCP provides a dedicated IDE suite. Users can use QCP through a VSCode plugin or the QCP web IDE. With QCP's IDE support, users can view the assertions satisfied by the current program state (i.e., intermediate results of symbolic execution) at any time while writing code, without needing to complete an entire function before verification.
QCP 2.0 Beta introduces AI-assisted verification. Users can now add annotations and complete Rocq proofs with AI assistance. QCP 2.0 makes verification smarter and more automated!
