本门课程大概讲述的是形式化方法(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里，可自行查看，如果老师助教看到了觉得不妥我就把这段删了。。）

1. 用Z3实现n-queens和逻辑加减法（slides已经给出公式了，调一下python API就行，代码也就几十行）
2. 用NuSMV验证一个简单的模型（slides已经给出几乎全部代码了，自己写下spec就行）
3. 编程大作业：有很多个选项，简单的如使用工具去求解：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. 各种拿了图灵奖的案例分析

作业基本上就是讲了什么就留什么：讲了理论就留一些理论的应用，讲了实践就留一个小实验。然后最后要求每个人至少做一个大实验。

没有考试。

另外老师讲的是真的好，这么多内容我一路听下来基本都能在课堂上弄明白。