2021春 课程号：CS400501
- 课程难度：中等
- 作业多少：中等
- 给分好坏：超好
- 收获大小：很多
| 选课类别：计划 | 教学类型：理论实验课 |
| 课程类别：本科计划内课程 | 开课单位：计算机科学与技术系 |
| 课程层次：专业方向 | 学分：3.0 |
形式化方法是硬件、软件、系统、协议设计的关键可靠性保障技术，可严格保证设计的正确性、安全性等，因此被列入各国的安全评估标准（最高级），如TCSEC、ITSEC等，并被广泛应用。由于网络与系统安全问题日益严重，操作系统、工业软件、芯片的设计复杂度逐步攀升，形式化方法已成为计算机各子领域的重点技术。
本课程介绍形式化方法的发展历程、当前现状及未来挑战；讲述形式化建模及验证的基础理论；通过当前各类主流形式化工具(包括Z3、NuSMV、ProVerif、Coq Proof Assistant等)的使用、比较、及经典案例解析，形成对形式化方法的综合理解。
课程内容： 《形式化方法导引》主要介绍了形式化方法的基础知识和实用工具，内容涵盖SAT/SMT Solver（DPLL & CDCL算法, Z3）、模型检测（LTL、CTL逻辑、Fix-point、ROBDD、NuSMV），以及简单介绍了ProVerif、Dolev-Yao Model和Pi-calculus。此外，课程前几周会快速回顾形式语言、自动机、命题逻辑、谓词逻辑和自然演绎。总体上，这是一门导引性课程，涉及内容广而不深，非常适合对形式化方法有兴趣的同学。
教学水平： 黄文超老师的讲课得到了一致好评，被认为“非常有条理，重点鲜明”。课程课件精美且实用，老师会在每节课结束前留出20分钟进行答疑，体现了对学生的耐心和关怀。所用课件还特别设计了不同版本，便于课堂展示和课后自学。
作业与考试： 作业和实验量较少且不难，具体作业包括PPT后面的练习题、Z3和NuSMV的小实验和一个自选的大实验。课程最后以大实验的形式进行考核，选题开放，可自由设计，老师鼓励大胆探索。本课程没有考试。
给分： 由于选课人数较少，加上学生普遍水平较高，黄老师与教务处沟通后，给到了40%以上的优秀率，因此给分相对友好。
总评： 总体来说，这门课被认为是“非常优质的课程，体验非常好”。内容涵盖面广但不深，适合同学们对形式化方法初步了解，尤其是对数理逻辑和编译原理感兴趣的同学。课内任务量较少，给分好，推荐大家选修。
- 课程难度：困难
- 作业多少：中等
- 给分好坏：超好
- 收获大小：很多
- 难度：困难
- 作业：中等
- 给分：超好
- 收获：很多
本门课程大概讲述的是形式化方法(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后面的练习（两周后交），以及 一个或两个自选题目（关于形式化）的大作业
老师上课真的很好，推荐大家明年来选
- 课程难度：简单
- 作业多少：很少
- 给分好坏：超好
- 收获大小：很多
- 难度：简单
- 作业：很少
- 给分：超好
- 收获：很多
出分了，来评个课。
首先老师讲课非常非常优秀，课件也非常非常用心，非常符合个人审美，给分也不吝啬（因为班里选课人数较少，与H班有不少重叠，老师跟教务处沟通后说给到40+优秀率是可以的）；而且很为同学着想，下课前会留20分钟给同学们答疑。
接下来介绍下课程内容，楼上已经讲得很清楚了，我就补充一点：没记错的话，这门课的内容基本上就是LogicInCS这本书加上一些补充，给我的感觉就是数理逻辑H。之前课程简介上说的coq什么的因时间原因并没有涉及。
然后谈一谈缺点：
- 可能是照顾大二学生，在逻辑部分讲得太多了，略有拖沓，而实际上在之前的数理逻辑课里，大三学生已经饱受直接证明摧残而十分熟练了（也可能因为我这学期当助教所以比较熟）。
- 个人觉得老师讲得还是有点浅，但考虑到是门导引课，这样也无可厚非。
- 作业布置的比较简单，七次小作业的总工作量还没数据隐私一次大。而且逻辑部分作业太多了（
- 讲的内容也没很展开，我去上交软院面试，谈到形式化，老师问的基本都是课上一笔带过的那种，给我一种我是不是啥也没学的感觉。
最后推荐各位同学选课，尤其是数理逻辑和编译原理自觉不错、并且稍微想学点东西的同学。大三下一门没有考试、作业简单、大作业时间宽裕的方向课，实在是很珍贵的。
为了防止后来的同学觉得课程太难不选，我描述一下本学期的实验作业吧（实际上都在课程主页的各PPT里，可自行查看，如果老师助教看到了觉得不妥我就把这段删了。。）
- 用Z3实现n-queens和逻辑加减法（slides已经给出公式了，调一下python API就行，代码也就几十行）
- 用NuSMV验证一个简单的模型（slides已经给出几乎全部代码了，自己写下spec就行）
- 编程大作业：有很多个选项，简单的如使用工具去求解：Z3求解矩形装箱、NuSMV验证deadlock；复杂一点就是实现算法：DPLL&CDCL，ROBDD；更高阶就是选CCF A&B论文自己去实现或者验证了（但根据自己的分数来看，应该没人选这个）
可见相比于其他课程实验，难度是不高的，再加上这门课没考试，所以emmm。总之，大家不要被课程名字和一些专有名词吓到了，虽然是个很深奥的领域，但导引这门课还是很轻松的。
- 课程难度：简单
- 作业多少：很少
- 给分好坏：超好
- 收获大小：很多
- 难度：简单
- 作业：很少
- 给分：超好
- 收获：很多
客观地讲，这门课确实是三年来上过的最优质的课程，体验非常好。
没有考试，作业也少，讲课效果也好，而且能感觉到学了不少东西。
最后考核方式是自选的大作业，也可以选很简单的任务。说真的，上完这门课，感觉最后给分多少已经无所谓了。
- 课程难度：中等
- 作业多少：很少
- 给分好坏：超好
- 收获大小：很多
- 难度：中等
- 作业：很少
- 给分：超好
- 收获：很多
课程内容：
包括理论和实际应用，详情可以参考其它评论。这是一门导引课程，所以会把许多方向都过一遍，但也不会在某一个方向上讲得太深。对于想要了解形式化方法的同学而言，这门课会是一个相当不错的选择，尤其适合喜欢数理逻辑/编译原理，或者对计算机理论感兴趣的同学。
讲课：
非常有条理，难能可贵的一点是详略有当，重点鲜明。很多东西直接平铺开来理解会把人困在复杂的迷宫里，但抓住一两条关键的脉络就能被迅速地领会。我认为黄文超老师在这门课的确做到了把课程内容的核心脉络讲清讲透，而非单纯地灌输定义和繁琐冗余的实现细节。
每节课后会留20min+的时间自由提问，几乎什么都能问，黄老师耐心地解答了我很多怪得有些离谱的问题，可谓是收获颇丰。
课件：
每节课主页上会准备两个版本的课件（不得不说黄老师的课件是咱用 Tex Beamer 做课件的开端）。一个适合用于上课展示，包含了动画演示，另一个在去掉动画演示的基础上新增了一些补充说明， 适合课下自学。
考试、作业和实验：
作业和平时的小实验量少且不难，没有考试，给分主要看期末的大实验，可以选择提交1-2个。大实验不限主题，可以自己自由设计，也可以参考老师给出的几个选题。大实验鼓励同学大胆地自行探索，最后看工作量和难度评价。因此如果自己对于这门课程有什么新奇的想法的话，大可以在大实验上实践一番。
给分：
由于这门课人很少，另外选课的人中大多也有点高能，因此老师与教务处那边做了沟通，允许给到40+的优秀率。所以给分很不错，不用担心养蛊导致给分暴死的情况。
- 课程难度：中等
- 作业多少：中等
- 给分好坏：一般
- 收获大小：很多
- 难度：中等
- 作业：中等
- 给分：一般
- 收获：很多
这门课程内容很多，而且也比较杂。不过总的来说知识不是特别深，还是很好懂的。
内容的话包含：
1. 自动机基础理论（让大家了解为什么形式化验证是一项很“难”的事务）
2. 命题逻辑、一阶逻辑、二阶逻辑和演绎推理（形式化验证的数学基础，基本上算是带大家复习一遍数理逻辑）
3. SAT/SMT的应用和求解理论
4. 模型检测LTL、CTL的应用和求解理论
5. 各种拿了图灵奖的案例分析
作业基本上就是讲了什么就留什么：讲了理论就留一些理论的应用，讲了实践就留一个小实验。然后最后要求每个人至少做一个大实验。
没有考试。
另外老师讲的是真的好，这么多内容我一路听下来基本都能在课堂上弄明白。
