ModelCheckingQNP¶

寻找一种能描述验证包括branch，while循环loop这类程序/controllor控制流图的“Logic”,先看IC3_Modelchecking

1. SAT-Based Model Checking without Unrolling

2. IC3 - Flipping the E in ICE

3. Understanding IC3

4. Efficient implementation of property directed reachability

软工方法论之形式化方法NuSMV学习笔记