QCP v2.1.2 fixes bugs in the MCP integration and symbolic execution of C structs, and adds a new MiniSAT verification result.
What's New
MiniSAT Verification
Added the verification of the MiniSAT SAT solver, including the annotated C implementation, generated verification conditions, and corresponding Rocq proofs.
- Annotated sources:
QCP_examples/Applications_human/minisat/ - Verification artifacts:
Rocq/examples/Applications_human/minisat/
Bug Fixes
- Fixed bugs in the MCP integration.
- Fixed bugs in symbolic execution involving C structs.
Happy verifying with QCP v2.1.2!