Part 1
Specification Annotations
Function pre/post-conditions, loop invariants, and IDE debugging feedback.
Tutorials
Tutorials
These tutorials cover four topics: specification annotations, memory and assertions, symbolic execution, and assertion extensions.
Part 2
Memory and Assertions
Common patterns with store, has_permission, and separating conjunction.
Part 3
Symbolic Execution
Verification conditions, control flow, assertion annotations, and loops.
Part 4
Assertion Extensions and Transformations
Mathematical predicates, custom separation-logic predicates, and automatic assertion transformations.
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 Generates Verification Conditions
During symbolic execution, QCP generates verification conditions (VCs). Every VC is an entailment between assertions: the assertion on the left of |-- must imply the assertion on the right, in the form P |-- Q. In essence, symbolic execution reduces checks for program safety and functional correctness to checks that these assertion entailments are valid. This tutorial first introduces two typical kinds of VCs that already appeared in earlier symbolic-execution examples. Later tutorials introduce more situations in which VCs are generated.
Read TutorialT3-4
Symbolic Execution for Conditional Branches and Control Flow
The following three C functions are possible implementations of absolute value. Here we use them only to illustrate a simple property: if the argument is not INT_MIN, then the function executes safely and returns a nonnegative value.
Read TutorialT3-5
Symbolic Execution with Assertion Annotations
QCP allows users to add assertion annotations between program statements to help complete verification. Loop invariants are one important kind of such annotation. When the QCP symbolic executor encounters an assertion annotation, it checks whether the strongest postcondition obtained so far implies the assertion manually provided by the user.
Read TutorialT3-6
Symbolic Execution for Loop Statements
We have seen that symbolic execution of assignments, if statements, and control-flow statements such as break, continue, and return is broadly similar to actual program execution. Loops are different: symbolic execution does not repeatedly execute the loop body until the loop exits.
Read TutorialAssertion Extensions and Transformations
T4-1
Using Mathematical Functions and Predicates in Specifications and Assertions
When a program and its intended behavior become more complex, simple arithmetic expressions may not be enough to state the intended function or the key assertions precisely. In that case, we can use additional mathematical concepts, including predicates and functions, to express the program's intent more clearly. These concepts help both developers and readers understand the code. However, using them often means that QCP's symbolic executor and solver cannot finish verification fully automatically. The user may need to complete some proofs manually in the Rocq theorem prover.
Read TutorialT4-2
Using Newly Defined Separation Logic Predicates in Specifications and Assertions
Sometimes it is convenient to treat all memory occupied by a data structure as a single predicate. For example, in C we can use the following struct to represent an ordered pair of integers.
Read TutorialT4-3
Automatic Demand-Driven Assertion Transformations in Symbolic Execution
Earlier we introduced the predicate store_int_pair, which treats the memory occupied by a struct int_pair as one separation-logic predicate.
Read TutorialT4-4
Other Automatic Assertion Transformations in Symbolic Execution
Earlier we saw that, when verifying operations on struct int_pair, QCP can unfold the store_int_pair predicate on demand during symbolic execution.
Read Tutorial