Part 1
Specification Annotations
Function pre/post-conditions, loop invariants, and IDE debugging feedback.
Tutorials
Tutorials
These tutorials cover three topics: specification annotations, memory and assertions, and symbolic execution.
Part 2
Memory and Assertions
Common patterns with store, has_permission, and separating conjunction.
Part 3
Symbolic Execution
Understanding QCP's execution through control flow, warnings, and assertions.
Specification Annotations
T1-1
Specification Annotations for C Function Safety
When verifying a C function, we need to specify its contract at the beginning of the function using annotations. This contract describes the function's safety or functional correctness. A C function's specification consists of a logical parameter list (With) and the corresponding separation logic pre- and postconditions (Require, Ensure). In simple cases, the specification may omit the With list.
Read TutorialT1-2
Using Assertion Annotations for Verification
If a program is relatively simple and the property to be verified is also straightforward, QCP can often complete the verification automatically. The examples such as add listed in T1-1 fall into this category. However, when programs become more complex -- even just by including loop structures -- QCP cannot complete the verification automatically. Users can employ assertion annotations to assist QCP in completing the verification. Among all assertion annotations, the most important is the loop invariant annotation.
Read TutorialT1-3
Viewing Symbolic Execution Results and Debugging
During program development and verification, it is common to not get the program right on the first try, and it can also be difficult to complete verification with annotations on the first attempt. QCP provides a companion VSCode plugin and a web-based IDE, allowing users to see intermediate verification results in real time.
Read TutorialMemory and Assertions
T2-1
Specification Annotations for Memory Operations
A key feature of C programs is their ability to read from and write to memory directly via memory addresses. For example, the following C program swaps the values at two addresses.
Read TutorialT2-2
Common Assertion Forms and Properties of Separating Conjunction
As we have seen in the preceding examples, the QCP assertion language supports the logical connectives && and *. The former denotes the usual logical "and", while the latter is the separating conjunction. Specifically, "P * Q" states that the current memory can be divided into two disjoint parts, one satisfying P and the other satisfying Q. We can use these connectives to combine multiple clauses and thereby express more complex concepts.
Read TutorialT2-3
Specification Annotations for Global Variables
If a and b are two signed integer global variables in a C program, then the following three versions of the swap_ab function can all swap their values.
Read TutorialT2-4
Specification Annotations for Struct Operations
If a C program defines the following struct struct int_pair, it is natural to use the previously defined swap function to swap the values of its two fields.
Read TutorialSymbolic Execution
T3-1
Simple Symbolic Execution
As previously introduced, symbolic execution computes the assertion that holds after a program statement executes, based on the assertion that held before it. Symbolic execution is one of the core modules of the QCP tool. Below, we use the swap function to illustrate the symbolic execution results for various program statements in QCP. The following is the swap function and its specification, which were introduced earlier. The QCP tool can automatically verify that the swap function indeed implements the functionality described by its specification.
Read TutorialT3-2
Basic Separation Logic Assertions
In the previously introduced swap function, there are two formal parameters px and py of integer pointer type, which can also be used as local variables within the function body:
Read TutorialT3-3
Symbolic Execution for Conditional Branches and Control Flow
The following three C functions are all potential implementations of computing the absolute value. Here we merely illustrate the verification of a simple property: if the argument passed to them is not INT_MIN, then they can execute safely, and their return value is non-negative.
Read TutorialT3-4
Symbolic Execution with Assertion Annotations
The QCP tool allows users to add assertion annotations between program statements to assist in completing verification. The loop invariant mentioned earlier is one such type of assertion annotation. When the QCP symbolic executor encounters an assertion annotation, it checks whether the strongest postcondition previously obtained through symbolic execution can entail the assertion manually provided by the user. Let us use the previously introduced swap function as an example.
Read Tutorial