教师：贺飞
助教：姜柏廷
线下答疑时间：每周三下午14:00~17:00
线下答疑地点：东配楼11-321
课程教学计划如下（暂定，可能根据实际教学情况进行调整）：
| 周次 | 日期 | 教学内容 | 助教 | 备注 |
|---|---|---|---|---|
| 1 | 2025/09/16 | 课程信息和概述 | ||
| 2 | 2025/09/23 | NuSMV工具 I | NuSMV安装及基本讲解 | |
| 3 | 2025/09/30 | NuSMV工具 II | ||
| 4 | 2025/10/07 | 放假不补 | ||
| 5 | 2025/10/14 | Kripke结构 | ||
| 6 | 2025/10/21 | 时序逻辑 I | 布置期中作业：NuSMV模型检验 | |
| 7 | 2025/10/28 | 时序逻辑 II | ||
| 8 | 2025/11/04 | CTL模型检验 | ||
| 9 | 2025/11/11 | LTL模型检验 期中小测 |
||
| 10 | 2025/11/18 | SAT模型检验 | 期中作业ddl：2025/11/17 23：59 布置期末作业：软件形式化验证 期中作业讲解 |
|
| 11 | 2025/11/25 | IC3算法 I | 讲解IC3 | |
| 12 | 2025/12/02 | IC3算法 II 期中小测讲解 |
||
| 13 | 2025/12/09 | 抽象-精化 | ||
| 14 | 2025/12/16 | 软件验证 I | ||
| 15 | 2025/12/23 | 软件验证 II | ||
| 16 | 2025/12/30 | 期末作业报告 | 期末报告 |