Now, let us look inside CBMC and figure out how cbmc works and how does it generate VC. We first download the slides explaining the first version (v1.0) of cbmc given by Daniel. That will help us understand cbmc’s structure.

## cbmc

### 前端处理 frontend

cbmc 的目标是分析 C/C++ 或者 JAVA 程序。CBMC 的第一步是输入程序，生成 CFG。关于如何生成 CFG，是编译原理的基础课程（我们可以用 CIL 来初步处理程序获得 CFG，另外，frama-c 平台也提供了现成的模块，可以直接获取）。

cbmc aims at the analysis of programs given in a commodity
programming language such as C, C++, or Java As the first step, it transforms the program into a control flow graph (CFG)

When we have the cfg, that means we have the execution paths of the programs. Thus, we can obtain the conjunction ($\phi_{i}$) of the condition in each joint point for each path $\phi_{i}$. The path will be executed if $\phi_{i}$ is valid.

let us look at the example in the above graph. We select one path and obtain the corresponding formula. This formula should be passed to a decision procedure and we obtain a satisfying assignment or the formula is invalid.

### SAT

SAT 的求解技术能力已经有了明显的提升。目前的很多研究是提高 word-level reasoningarray decision procedures 的效率。

## Transition System

A transition system $(S, T, I)$ is defined as follows:

• a set of states $S$;
• a transition relation $T: S \rightarrow S$;
• a set of initial states $S_{0}\subseteq S$.

A program is modelled as a transition system. Each state of the program is an evaluation of all variables in the program. Each state may has many possible successors, i.e., the transition relation is non-deterministic.

Example1 : $S = \{a,b,c\}$, $I = \{a\}$ and $T = \{ \langle a,b\rangle, \langle b,b\rangle, \langle b,c\rangle\}$

## 总结

cbmc 的步骤总共有三步：

1. 前端处理，获得程序的 cfg
2. 展开 unwind cfg，获得路径的公式
3. 利用 SAT/SMT 求解公式