This is the first release version of Qualified-C-Programming (QCP).
QCP is a C program verification tool. Given an annotated C program as input, QCP performs symbolic execution and generates verification conditions to be verified in Rocq.
In version v1.0, we provide executable files for three different systems—Linux, Windows, and macOS (ARM64)—along with a Rocq library for verification and a VS Code extension that allows users to view the results of symbolic execution in real time.