形式化方法导引(黄文超) 2021春  课程号:CS400501
2021春  课程号:CS400501
10.0(1人评价)
  • 课程难度:困难
  • 作业多少:中等
  • 给分好坏:一般
  • 收获大小:很多
选课类别:计划 教学类型:理论实验课
课程类别:本科计划内课程 开课单位:计算机科学与技术系
课程层次:专业方向 学分:3
点评 写点评
farmerzhang1 2021春

本门课程大概讲述的是形式化方法(Formal Methods)的一部分

具体地说,是

SAT/SMT Solver (DPLL & CDCL算法, Z3)

和Model Checking(LTL, CTL逻辑, Fix-point, ROBDD, NuSMV)

最后一节课简单介绍了ProVerif, Dolev-Yao Model, Pi-calculus(让我意识到形式化这个坑有多么的深

没有讲Coq

 

以及开学前几周会非常快速地过掉formal languages 和 automata 还有命题逻辑 谓词逻辑 自然演绎

作业是ppt后面的练习(两周后交),以及 一个或两个自选题目(关于形式化)的大作业

老师上课真的很好,推荐大家明年来选

2021-06-05 13:52 4 0

黄文超

教师主页: 戳这里

其他老师的「形式化方法导引」课

黄文超老师的其他课

操作系统 7.8 (5) 2020秋 2019秋...
现代密码学理论与实践 5.2 (9) 2020秋 2019秋...
操作系统 2017秋