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.
What's New
🔍 LLM‑Powered QCP Verification Enhancements
- Optimized the end‑to‑end process for using LLMs in QCP verification, including improved prompting strategies and skill definitions.
- Added a comprehensive set of examples demonstrating LLM‑based verification in
QCP_examples/LLM_bench.
🧵 String Literal Symbolic Execution
- QCP now supports symbolic execution of string literals, enabling more precise analysis of programs that manipulate constant string values. This improves verification coverage for string‑related operations and constraints.
📚 New Verification Libraries
- Added GraphLib – a collection of verified graph algorithms and data structures to facilitate reasoning about graph properties.
- Added MinMaxLib – a library for min‑max computations with formal correctness proofs.
- Both libraries are located under
SeparationLogic/and are ready to be imported into your QCP specifications.
Improvements
- Refined the skill definitions used during LLM‑assisted verification, reducing false positives and improving convergence.
- Update a new SMT solver to make symbolic execution faster.
Bug Fixes
- Fixed a rare issue for extension display and ubs in symbolic execution.
We appreciate your feedback! Please report any issues on our issue tracker or contact the team directly.
Happy verifying with QCP v2.0.2!