Skip to content

QCP-v1.0

Choose a tag to compare

View all tags
@yashen32768 yashen32768 released this 28 Mar 12:08
· 19 commits to main since this release
v1.0
af71be0

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.

In version v1.0, we provide executable files for three different systems—Linux, Windows, and macOS (ARM64)—along with a Rocq library for verification and a VS Code extension that allows users to view the results of symbolic execution in real time.

Assets 2
Loading