最新版本稳定版
QCP-v2.1.0
QCP-v2.1.0
We are pleased to announce QCP v2.1.0. This release is centered on two major milestones: Lean proof-backend support and a substantial update to the verified CDCL SAT solver example.
全部版本
7 Releases稳定版
QCP-v2.0.4b
QCP-v2.0.4b
QCP v2.0.4b is a maintenance release for the v2.0.4 line. It focuses on bug fixes, a broader example set, improvements to the LLM-assisted proof workflow, and a refreshed QIDE extension.
稳定版
QCP-v2.0.4
QCP-v2.0.4
We are pleased to announce QCP v2.0.4. This release expands the C programs that QCP can verify and makes complex verification failures substantially easier to diagnose. It introduces a more complete C preprocessor, floating-point verification, pointer-offset reasoning, reusabl...
稳定版
QCP-v2.0.3
QCP-v2.0.3
We are excited to announce the release of QCP v2.0.3! This update focuses on improving AI-assisted proof migration, expanding the verified example suite, refreshing the cross-platform verification toolchain, and adding new libraries for symbolic execution and formal reasoning.
稳定版
QCP-v2.0.2
QCP2.0.2
We are excited to announce the release of QCP v2.0.2! This update focuses on enhancing LLM‑driven QCP verification workflows, expanding symbolic execution capabilities, and adding new supporting libraries to simplify verification tasks.
预览版
QCP-v2.0beta
v2.0beta
We are excited to announce the release of QCP v2.0beta! This update focuses on bridging the gap between Large Language Models (LLMs) and formal verification. By introducing qcp-mcp and rocq-mcp , we have enabled AI agents to interact directly with QCP, allowing them to autonom...
稳定版
QCP-v1.0
v1.0
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.