道歉信

尊敬的老师、助教：
感谢你们在一学期的教学付出，使这门课有精美的PPT、优质的授课和及时的解答。可以看得出来各位工作者也很希望把这门课做成一门优秀的课程。

可惜我实在是太菜了，我也很想好好的回看PPT和讲义，但是我不仅没时间还懒，真的很愧对老师和助教的付出。我的作业从第三次开始就没怎么好好写，实验也只能做一个很勉强的版本，大作业的质量也十分堪忧。这门课拓宽了知识面，但是很遗憾，我没有做详细的了解，很多老师讲过的东西我也忘了。

作为一个失败的学生，我只能在这里勉强写一个作业以获得一个及格分数，我保证出去不说是你教的，以免败坏了各位老师的名声。在此我只能献上一份道歉了。再次感谢老师和助教的努力，祝老师助教事业顺利、生活幸福。

占

大概是这个学期最能听的一门课

作业反馈一点不及时，学期内的每次作业要求大家按时交，逾期扣分。自己却拖到期末之后再改，嘴上说着一天能出分，最后拖10天。。。

在批改大作业的过程中则是在群里声称发现很多同学存在抄袭行为，希望同学们主动发邮件坦白，搞得半夜十二点半起码十几二十个人睡不着觉。。。。为什么不能直接私聊抄袭的同学呢？

给分方面，完全没有想象的那么奶，完全就是严格给分，以致于很多同学掉大分。。做了整整一周的大作业最后就给了3.0 。。。

教学方法：10/10

这门课全部由黄老师讲授，解围老师可能只是挂名的。

黄老师应该是我这学期上的课老师里讲课最好的了，讲课深入浅出，一点也不枯燥。老师会提前把上课用的slide放在自己的主页上，可以自取。上课的时候还会有板书讲解与实机演示。

看得出来，老师对教学还是很认真的，会听取同学的反馈对课堂教学作调整。这门课到今年为止开了三年，大概老师也在不断地改进教学。

这门课在周五的8/9/10三节，每次老师大概讲到六点多一点就会下课，之后的时间就是留给大家提问的，可以自行上台找老师探讨问题。课后老师也会在QQ群里回复大家的疑问啥的。

课堂内容：10/10

这门课从经典数理逻辑开始，介绍了逻辑问题求解(SAT/SMT问题定义，Z3，DPLL，CDCL，单纯形法等)，模型检测(LTL/CTL，NuSMV，不动点，ROBDD等)以及一些案例分析(ProVerif，抽象解释，CEGAR，Coq等)。因为是导引，所以没有太深的内容，但有些内容还是很有难度的。

作业实验：8/10

这门课没有考试，一共是6次作业，3次小实验和1次大实验。

作业部分布置在slides最后面，难度都不高，最多的一次应该是4道题，不过耗时最多的一次应该是ROBDD那次的作业画图。课后过一遍slides，顺着slides里的例子应该就可以把作业做出来。

小实验也布置在slides最后面，基本都是把slides里给出的代码进行一定的修改即可。比较有难度的一次应该是死锁的条件转换成CTL语句。

大实验可以从以下一些内容中选择着做，括号里是对应的slides编号：

1. (4)分别用 Z3 和自己设计的算法求解 rectangle fitting。要求：代码: (1) 使用 Z3 实现 PPT 中的设计 (2) 自己设计算法（使用 C、C++ 语言等）文档: (1) 解释自己的算法思路 (2) 设计测试集，对比两个方法的效率

2. (4.2)自行设计 CNF 的 SAT 求解算法, 要求:可以使用现有算法 (如 DPLL, CDCL)，也可以自行设计其他算法；可以独立设计可执行程序，也可以修改现有开源程序的核心算法（选取后者分数更高）；自己构建测试集（可网上查找测试集）；附上详细的文档: 包括实现过程，算法解释，与现有工具 (如 Z3)等的性能对比

3. (5.1.4)选择一篇 CCF A 类论文，自己用 NuSMV 设计论文中的模型，并验证，附完整文档。
(也可选择 NuSMV 中 example 中的 A 类论文, 对已给出的模型进行阅读，并附完整的阅读、试验报告、以及心得体会)

4. (5.1.4)实现 PPT 中的 deadlock 验证，并针对complicated example 中所给的结论进行验证。要求附上源码和实验报告

5. (5.2)实现 ROBDD 算法, 要求:可以实现至不同 stage，例如，可实现至 ROBDD, 或 ROBDD-CTL。
实现的越完整，给分越高。提供源代码、可执行程序、测试文件、相关文档

6. (6.1)做 ProVerif 相关的大实验。题目开放，下面为参考选题，但不限于下面选题
选题 (1): 使用 ProVerif 验证更复杂安全协议, 可模仿一下 CCF A，B 类论文，来进行建模, 并成功验证
选题 (2): 尝试设计核心验证算法，改进 ProVerif 的验证效率
选题 (3): 阅读其它验证器的论文和代码，自己模仿设计新的验证器, 或修改核心模块 (不要求完整实现，可以只包含核心求解算法)
注：评分标准根据实现难度和工作量来评定，不要求完整实现所有内容, 上述实现需尽可能提供完整文档
 

另外选择自己感兴趣的和这门课有关的内容作为大实验应该也是可以的。大实验可以提交两份。

老师对复现论文比较青睐，课堂上提到了很多次。不过估计最后也没有太多人去卷这个。

这个部分给8分一是因为反馈不及时，学期中间只出了hw1的分数，而剩下的分数都是在所有实验全部提交之后才出的(老师还在群里说可能大实验交上去之后一天就能把分数全给出来，结果花了十天，笑)；二是因为小实验的文档要求和最后的评分有点不太一致。

收获如何：10/10

在学这门课之前，我完全不了解什么是形式化方法。学完之后，应该可以算是对这个领域有了一个入门式的认知，收获还是很大的。

总体评价：9/10

这门课还是很推荐选的。不过老师好像对今年的到课率不是很满意，据说明年会加入点名。

以下和评课无关：

助教：这门课有两位助教，会随堂听课，学期末的习题课上助教把作业都讲解了一遍，但可能是因为没有考试，认真听的人不多。

老师觉得大实验的分数和考试一样，应该不出分而直接把总评提交给教务处，要是个人有异议的在出总评之后可以再联系老师。个人不是很认同老师的做法。不过在出总评之后老师把大实验的分数放在了bb上面。

上课&内容：
其他评课已经讲述的十分清楚了，老师上课的确非常认真负责且讲的很好，但是写作业的时候会发现有些需要用到的内容在讲课中并未提及，在对老师上课态度的负责上我十分尊重，正因此不会打1分。

作业&实验：
这门课的作业几乎全部是学期末所有作业&实验全部提交后进行给分的，在作业中并未明确表明什么内容应该被提及以及一个粗略的标准，但是(据我了解的很多人)都被扣了很多分，这里的疑问是，严格判罚作业并无问题，但是否应该每次作业都给予一定的反馈，否则每次作业出现的纰漏和未提及的内容作为一个学生我确实无法意识到。

大作业&给分：
2023春的背景是老师在群里说“有人是用GPT生成/抄袭的”，会给这样的大作业低分/挂科，我不知道是否与这个背景相关，做PPT后提到的内容，相比起做非PPT提到的大作业内容，都给出了极低的分数。也就是说，你从头写一个ROBDD的实现，远不如别人找教程用nusmv或其他工具+教程实现的验证来的分高，可悲的是也许工作量是差不多的。我不知道老师对此的用意为何，老师上课曾强调数次"课后的大作业选题是实在找不到题目才做的"，难道就因为这个就可以直接爆杀掉做课后大作业的？就直接认为做课后大作业的都是屑，垃圾，直接低课外大作业n等？如果这样的话你不要放大作业的内容直接让大家找不好吗？何必要给出这样的题目？如果是为了有抄袭直接一竿子打死所有做往年已有的题目的，那我的评价是不会查就别查了

┭┮﹏┭┮

上课应该还好，虽然我很多时候都听不懂，经常感觉自己的关注点和授课的关注点不一致；一直到model checking基础部分体验都还比较好，后面感觉真的力不从心。

作业体验确实不好，作业里算法遇到的情况大大超出了课题上示例的范围，而且我不认为这是通过思考和不多的参考就能解决的问题，典型如最后一次作业的widening、narrowing等。

课程最好的还是老师的答疑了，黄老师一定是我上过所有课程中答疑解惑最及时的了，课程群里的消息感觉1/4-1/3都是老师发的，(感动）,这点在学习过程中帮助挺大。对比一下助教的工作，，，，，，，ƪ(˘^˘)ʃ

我的大作业经历是，来回看了一圈，写了个最简单的，明明时间还是比较足的，却啥也没干。不过还是不喜欢老师这种看paper大于写labs in slides的导向，主要我找了一圈没找到足够简单复现的（哭笑）

收获吧，算是对这个领域有了初步的认识，但其中很多内容确实很难让我感兴趣，不过也有个人比较喜欢的部分，如LTL等逻辑部分，coq证明工具

不是一门水课，抱着水学分心态来选的同学快跑

优点：

• 考勤：本学期无考勤，但是以后很可能会有
• 老师：老师本人经常在群里解答问题，也比较乐意听取意见；承诺不随意挂人
• PPT：在课程主页上及时发布，方便用电脑边听边做笔记

缺点：

• PPT：全英文，而且真的就是用来上课的，不是讲义，自学的话非常痛苦
• 作业：作业文档不给出详细要求，到了改作业的时候按「没有过程」等等之类的理由扣分（在本人反馈之下取消了CNF题的扣分）；扣分非常严格，没有保底分，看到有同学交了然后判0分的，乐
• 助教：
  • 助教到了整门课结束的时候才上习题课、讲作业，早都忘记怎么做的了
    • 因为这门课作业祖传，习题课PPT也不发，没法更正
  • 助教到了期末才改作业，有种根本不在乎我们学习效果的感觉。不过这也无可厚非，计算机学院是这样的
• 老师：在群里说有人大作业GPT生成/抄袭，也不说是谁，就要求发邮件说明情况，大可不必吧？

大作业：

• 本人大作业尝试复现了一个CCF A类文章的证明（数学定理的Coq形式化及证明，也没完全复现，太难了），然后针对复现过程编写了一个小工具（真的很小），最后给分还可以

这门课是数理逻辑的升级版，

我学的不好，大致意思是把问题表示成变量的表达式(形式化)，条件包含3个公理等，然后用搜索、剪枝、线性规划等技术，在解空间里求符合条件的解答

最后一部分是用符号和公理证明数学定理，比较有意思，最近有个新闻也是在干这个，https://www.jiqizhixin.com/articles/2024-01-31-5

黄老师最后还向我们请教建议，那时候也没认真学，

现在想起来有个很重要的问题是 对这门课没有一个清晰的认识，每个星期都是按照老师讲的算法写点作业，感觉知识点很零碎，要是老师可以帮我们分析一下这些知识点之间的联系，再结合实际应用的话就更好了，

事少，给分好，善于接受反馈，绝对值得选

em 我在外实习 邮件问熊老师说会做录像

但是目前似乎没有上传 有在校上课的同学能告知一下课程群吗（若有）