教师：贺飞
助教：韩志磊、黄碧婷
教师答疑时间：每周五下午16:00~18:00
教师答疑地点：东配楼11-307
助教答疑时间：每周二下午14:00~17:00
助教答疑地点：东配楼11-321
考核方式：
期末考试时间：待定 期末考试地点：待定
课程教学计划如下（暂定，可能根据实际教学情况进行调整）：
| 周次 | 日期 | 教学内容 | 讲义 | 作业 | 备注 |
|---|---|---|---|---|---|
| 1 | 2026/02/27 | 绪论 | |||
| 2 | 2026/03/06 | 命题逻辑 | |||
| 3 | 2026/03/13 | 一阶逻辑 | |||
| 4 | 2026/03/20 | 一阶理论 助教课：Z3工具（时间另行通知） |
Homework 1 逻辑 (DDL:03/26) | ||
| 5 | 2026/03/27 | IMP程序语言及其语义 | |||
| 6 | 2026/04/03 | 霍尔证明系统 | |||
| 7 | 2026/04/10 | 深入理解循环 扩展IMP语言–数组 |
|||
| 8 | 2026/04/17 | 最弱前置条件 | Homework 2 程序的语义 (DDL:04/23) | ||
| 9 | 2026/04/24 | 扩展IMP语言–过程 助教课：课程大作业说明 |
|||
| 10 | 2026/05/01 | 五一放假 | |||
| 11 | 2026/05/08 | 程序终止性 | Homework 3 演绎验证 (DDL:05/14) | ||
| 12 | 2026/05/15 | 推导循环不变式 | |||
| 13 | 2026/05/22 | 程序的自动机表示 | |||
| 14 | 2026/05/29 | 自动程序验证（1） | |||
| 15 | 2026/06/05 | 自动程序验证（2） | |||
| 16 | 2026/06/12 | 扩展性内容 |