教师:贺飞
助教:谢兴宇、韩志磊、徐志杰
教师答疑时间:每周五下午15:00~17:00
教师答疑地点:东配楼11-307
助教答疑时间:每周三下午14:00~17:00
助教答疑地点:东配楼11-321
课程教学计划如下(暂定,可能根据实际教学情况进行调整):
周次 | 日期 | 教学内容 | 讲义 | 作业 | 备注 |
---|---|---|---|---|---|
1 | 2023/02/24 | 绪论 | |||
2 | 2023/03/03 | 命题逻辑 | 2 | ||
3 | 2023/03/10 | 一阶逻辑 | 3 | Homework 1 (DDL:03/23) | |
4 | 2023/03/17 | 一阶理论 助教课:Z3工具(时间另行通知) |
4 | ||
5 | 2023/03/24 | IMP程序语言及其语义 | 5 | Homework 2 (DDL:04/06) | |
6 | 2023/03/31 | 演绎程序验证 | |||
7 | 2023/04/07 | 循环 |
Homework 3 (DDL:04/20) | ||
8 | 2023/04/14 | 验证条件 | |||
9 | 2023/04/21 | 扩展IMP语言 助教课:课程大作业说明 |
Homework 4 (DDL:05/11) | ||
10 | 2023/04/28 | 程序终止性 | |||
11 | 2023/05/05 | 放假 | |||
12 | 2023/05/12 | 推导循环不变式 | |||
13 | 2023/05/19 | 程序的自动机表示 | |||
14 | 2023/05/26 | 自动程序验证(1) | Homework 5 (DDL:06/01) | ||
15 | 2023/05/30 | 自动程序验证(2) | |||
16 | 2023/06/02 | 扩展性内容 |