Skip to content

QCP-v2.1.3

Choose a tag to compare

View all tags
@yashen32768 yashen32768 released this 21 Sep 14:58
· 3 commits to main since this release
QCP-V2.1.3
47d4a34

QCP v2.1.3 Release Notes

QCP v2.1.3 fixes bugs in symbolic execution and Coq/Lean goal generation, and marks QCP's support for the first online preliminary round of the Second Theorem Proving Competition.

What's New

Supporting the Second Theorem Proving Competition

QCP supported the first online preliminary round of the competition's Human–AI Collaboration track, held on September 20, 2026. Participants used QCP or CStar with AI assistance to solve five program verification problems during a two-hour contest.

Across the two platforms, 29 participants submitted solutions, and 10 completed all five problems. Congratulations to all participants!

The second online preliminary round is scheduled for October 10, 2026. We welcome everyone interested in AI-assisted program verification to participate.

For results and participation details, see the competition report.

Bug Fixes

  • Fixed bugs in floating-point conversions, empty for loops, and negative constants.
  • Fixed predicate renaming in the Coq and Lean goal printers.
  • Fixed record-array field readback and preserved symbolic index matching.

Improvements

  • Updated the QCP binaries for Windows, Linux, macOS arm64, and macOS x86-64.
  • Refreshed generated Rocq verification conditions and proofs for affected examples.

Happy verifying with QCP v2.1.3!

Assets 2
Loading