课程主页 --《形式化方法导引》

课程信息

课堂信息
上课时间 周五 15:55
上课地点 3A107
上课周数 1-14
联系方式
主讲教师 黄文超
助教 付贵禄
Email (助教) fuguilu@mail.ustc.edu.cn
QQ群

课件 (更新中...)

0. 课前准备
PPT

第1章 绪论
PPT Noted Slides

第2章 经典数理逻辑--问题定义
PPT Noted Slides

第3章 经典数理逻辑--问题求解基础
PPT Noted Slides

第4章 逻辑问题(SAT/SMT)求解
4.1 应用
PPT Noted Slides

第4章 逻辑问题(SAT/SMT)求解
4.2 理论 4.2.1 SAT求解
PPT Noted Slides

第4章 逻辑问题(SAT/SMT)求解
4.2 理论 4.2.2 SMT求解
PPT Noted Slides

第4章 逻辑问题(SAT/SMT)求解
4.2 理论 4.2.3 CNF与Horn Clauses
PPT Noted Slides

第5章 模型检测
5.1 应用 5.1-3 Model checking | LTL | CTL
PPT Noted Slides

第5章 模型检测
5.1 应用 5.1.4 NuSMV
PPT Noted Slides

第5章 模型检测
5.2 理论 5.2.1-2 Basic idea: Fixpoint | BDD
PPT Noted Slides

第5章 模型检测
5.2 理论 5.2.3-4 BMC | K-induction
PPT Noted Slides

第6章 案例分析
6.1 ProVerif: A Verifier of Security Protocols
PPT Noted Slides

第6章 案例分析
6.2 Coq: A Prover based on Higher-order Logic
PPT Noted Slides

第6章 案例分析
6.3 Event B: A Prover based on First-order Logic
PPT Noted Slides

实验简明教程 (感谢付贵禄同学提供的文档) (更新中...)

Z3 使用教程 DOC

NuSMV 使用教程 DOC

参考书目