Skip to content

QCP-V2.1.2

Choose a tag to compare

@yashen32768 yashen32768 released this 14 Sep 16:26
· 4 commits to main since this release

QCP v2.1.2 Release Notes

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!