1显式状态模型检查
闭卷重建显式状态模型检查的对象、公式、算例、算法与失败边界。
形式化方法与程序验证 · 小纸条
选一章打印。双面打印（按长边翻页）后沿虚线剪开，每张卡片正面题目、背面答案。
第 1 页 · 正面（题目）
2状态爆炸
闭卷重建状态爆炸的对象、公式、算例、算法与失败边界。
3偏序约简
闭卷重建偏序约简的对象、公式、算例、算法与失败边界。
4对称约简
闭卷重建对称约简的对象、公式、算例、算法与失败边界。
5BDD符号模型检查
闭卷重建BDD符号模型检查的对象、公式、算例、算法与失败边界。
6有界模型检查
闭卷重建有界模型检查的对象、公式、算例、算法与失败边界。
7归纳模型检查与k-induction
闭卷重建归纳模型检查与k-induction的对象、公式、算例、算法与失败边界。
第 1 页 · 背面（答案）
对象：并发组件全局状态是局部状态笛卡尔积，再乘变量和队列取值。；公式：|S_global|≤∏|S_i|。；算例：5个组件各4态，上界4^5=1024。；边界：只报代码行数判断可验证性。。
对象：显式检查枚举可达状态和转移，使用visited避免重复并在坏状态重建路径。；公式：time=O(|S|+|R|)。；算例：100状态300转移，线性工作代理400。；边界：可变状态哈希；对称状态重复爆炸。。
对象：身份可交换的同构进程状态归一到代表，减少重复。；公式：canonical(s)=min_{π∈Sym}π(s)。；算例：两个同构进程局部态A,B，(A,B)与(B,A)归为一类。；边界：性质点名某进程破坏对称仍约简。。
对象：独立动作的不同交错若对性质等价，可只探索代表顺序。；公式：a∘b=b∘a且互不影响启用性。；算例：两个独立动作有ab、ba两种交错，约简可保留1种代表。；边界：把共享读写动作误判独立；活性性质未满足约简条件。。
对象：BMC把长度≤k的路径和性质否定编码为SAT/SMT，找到短反例但无反例不自动证明全局。；公式：I(s0)∧∧_{i<k}R(si,si+1)∧Bad(sk)。；算例：k=3编码含状态s0到s3共4层。；边界：k内无反例就宣称永远安全。。
对象：BDD用共享决策图表示大状态集合与转移，变量顺序决定规模。；公式：Reach_{i+1}=Reach_i∪Post(Reach_i)。；算例：三位状态集合可用8个显式位；BDD可能共享子图但最坏仍指数。；边界：把BDD称为总能避免爆炸；动态重排改变性能未记录。。
对象：基例检查前k步，归纳步假设连续k状态安全并证下一状态安全。；公式：Base_k ∧ Step_k。；算例：1-induction失败可能是归纳假设太弱；加入辅助不变量后可成功。；边界：归纳步反例直接当真实系统反例。。