Homepage

《软件分析与验证》2024年春季学期

教师:贺飞

助教:韩志磊、黄碧婷


教师答疑时间:每周五下午15:00~17:00

教师答疑地点:东配楼11-307


助教答疑时间:每周二下午14:00~17:00

助教答疑地点:东配楼11-321


期末考试时间:2024-06-16(周日) 14:30~16:30 期末考试地点:明理楼-112


课程教学计划如下(暂定,可能根据实际教学情况进行调整):

周次 日期 教学内容 讲义 作业 备注
1 2024/03/01 绪论 1    
2 2024/03/08 命题逻辑 2    
3 2024/03/15 一阶逻辑 3 Homework 1 (DDL:03/23)  
4 2024/03/22 一阶理论
助教课:Z3工具(时间另行通知)
4    
5 2024/03/29 IMP程序语言及其语义 5 Homework 2 (DDL:04/06)  
6 2024/04/07 霍尔证明系统 6   调课
7 2024/04/12 深入理解循环
扩展IMP语言–数组
7, 8 Homework 3 (DDL:04/20)  
8 2024/04/19 最弱前置条件 9 Homework 4 (DDL:05/11)  
9 2024/04/26 扩展IMP语言–过程
助教课:课程大作业说明
10    
10 2024/05/03       放假
11 2024/05/10 程序终止性 11    
12 2024/05/17 推导循环不变式 12    
13 2024/05/24 程序的自动机表示 13 Homework 5 (DDL:06/01)  
14 2024/05/31 自动程序验证(1) 14, 15    
15 2024/06/07 自动程序验证(2) 16    
16 2024/06/14 扩展性内容