Books
Handbook of Model Checking（选读卡片）
为何放进书单
手册体例适合「用到哪查到哪」。做 AI4EDA 验证闭环时，常需快速对齐 BMC、抽象、组合电路验证等术语。
当前进度
- 状态：
reference（不当线性读物，按需翻）。 - 已粗读：SAT-based model checking、equivalence checking 相关章节索引。
- 计划精读：与硬件验证案例更近的章节，笔记输出到
/notes。
和站点其他栏目的关系
- 论文卡片提供「一篇一文」的前沿切片；本书提供稳定定义与算法骨架。
- 定理证明笔记中的不变量表述，应能在手册术语下找到对应物。