TODO:
- FT generation
- Diagnosis
PAPERS:
*
CODE:
CONFUSIONS:
*
CONCLUSIONS:
- Symbolic Execution 和 Model Checking的区别
- 确定性程序和不确定性：把不同的程序块（一个入口进一个入口出）看作不同状态，确定性程序即静态程序：程序块的执行顺序确定（sequential的）；不确定性程序，如并发程序，的程序块执行顺序是不确定的：如线程A执行后，线程B,C,...N都可以继续执行，这就是不确定的。
- SE是针对静态程序，symbol的是程序的某些变量：可以是输入变量，可以是程序里的某些变量（如分支条件等）
- MC针对程序状态转移不确定的程序（但得是有限的状态转移），检查不同的执行顺序（全部状态空间）下最终程序终止时的状态，还有一个前提是这些不确定转移顺序的程序块一定会对共享数据进行读写，否则也不需要MC了