形式化方法导引(熊焰, 黄文超, 解围) 2022春  课程号:CS400501
2022春  课程号:CS400501
8.3(6人评价)
  • 课程难度:中等
  • 作业多少:中等
  • 给分好坏:一般
  • 收获大小:一般
选课类别:计划 教学类型:理论实验课
课程类别:本科计划内课程 开课单位:计算机科学与技术系
课程层次:专业选修   学分:3.0
简介 最后更新:

形式化方法是硬件、软件、系统、协议设计的关键可靠性保障技术,可严格保证设计的正确性、安全性等,因此被列入各国的安全评估标准(最高级),如TCSEC、ITSEC等,并被广泛应用。由于网络与系统安全问题日益严重,操作系统、工业软件、芯片的设计复杂度逐步攀升,形式化方法已成为计算机各子领域的重点技术。

本课程介绍形式化方法的发展历程、当前现状及未来挑战;讲述形式化建模及验证的基础理论;通过当前各类主流形式化工具(包括Z3、NuSMV、ProVerif、Coq Proof Assistant等)的使用、比较、及经典案例解析,形成对形式化方法的综合理解。

排序 学期

评分 评分 6条点评

yomia 2022春
  • 课程难度:中等
  • 作业多少:很少
  • 给分好坏:超好
  • 收获大小:很多
  • 难度:中等
  • 作业:很少
  • 给分:超好
  • 收获:很多

这学期授课全部由黄老师完成,解围老师担任助教。

黄老师上课很用心,也讲得很好,而且很积极与学生互动,经常阶段性地关心同学们有没有听懂,每次课都会留半小时左右的时间给同学们课后提问。

内容方面,前期主要是回顾和拓展了数理逻辑相关知识,后面会介绍该领域的一些基本知识和一些软件工具,印象最深的有SAT问题的求解、模型检测(NuSMV,LTL/CTL)(因为大作业做的是这两个hh)。知识方面个人觉得在理解上有一定难度,但是认真听老师讲课和认真独立完成作业对理解有很大帮助。虽然知识理解起来不容易,但是作业和小实验难度是OK的,个人觉得不属于简单,但是只要理解了就能很顺利地完成那种。

有9次平时作业(包括书面小作业和3次小实验好像)和一个大作业,大作业最后实现了DPLL算法来求解SAT和用NuSMV验证死锁(PPT上有说明),做两个是因为觉得这两个都属于工作量相对不大的那种。最后写得比较匆忙,平均每个花了两天时间,自我感觉不是很好,很多地方都没有完善,实验文档也写得很匆忙、不详细,以为有3.3就很感激了。

最后总评98,在科大本科最后一门知道成绩的课,也是在科大成绩最高的一门课,属于是喜出望外了!

黄老师,解老师,我的超人!

 

---------------------------------以下内容为2022秋季学期更新--------------------------------------------------------

第一次体会到简历match是什么感觉。将这门课的大作业搬到了简历上,多亏这个获得了一个实习offer,面试官聊得最多的就是SAT问题(中间还聊到了SMT问题但我当时没想起来),后面发现z3,SMT这些都用起来了。再次感谢黄老师!

(最后修改于 4 1 复制链接
红领巾梁神?
立即登录,说说你的看法
Catoverflow 2022春
  • 课程难度:中等
  • 作业多少:很少
  • 给分好坏:一般
  • 收获大小:很多
  • 难度:中等
  • 作业:很少
  • 给分:一般
  • 收获:很多

12给黄老师,8分给解助教老师,平均一下。黄老师上课真的非常认真,每次讲完知识点都会说有没有讲清楚,如果有同学说没理解还会再讲一遍。最后大作业评价的问题也是黄老师一起解决的,真的是我在科大碰到的最负责的老师之一。黄老师的口头禅是“事实上”,但是这个词听多了还是容易没搞懂事实上是什么。

形式化方法这门课一定程度上是数理逻辑的后继,但是数理逻辑没学好影响不是很大(比如我);此外内容上和人工智能的 logic agent 部分有一定重合,教授的时间也是重合的,所以一起上非常舒适。一个老师的课没听懂可以看另一个老师解释


顺便,我还是觉得我的工作被低估了(看到上面一个98的酸了,我做了没人实现过的 LALR+ROBDD constructor 也没有拿到这个成绩)

(桃子部分,不知道老师能不能看到)如果以后上课讲到 ROBDD 需要一个可视化的公式到 ROBDD 即时构建器,可以用我这个,到时候可以考虑出个 windows release;学到了这个部分想自己玩玩的同学有也可以来看看

(最后修改于 3 1 复制链接
红领巾“事实上”,太真实了
立即登录,说说你的看法
腕豪 2022春
  • 课程难度:困难
  • 作业多少:很少
  • 给分好坏:超好
  • 收获大小:很多
  • 难度:困难
  • 作业:很少
  • 给分:超好
  • 收获:很多

这门课名字叫做形式化方法,我选这门课之前也不知道这门课是干啥的,只是因为这门课没有考试才选的,学完之后发现这门课真的不错。我觉得这门可以算作是对数理逻辑的扩展(这样说其实也不太准确,但是由于如果没学过这门课的内容,也不太好解释清楚,所以可以看作是数理逻辑的扩展)

这门课的内容挺难的,但是只要上课跟着老师的思路走,别玩手机,听懂是没有问题的,只要听懂了,课后的作业也比较简单。由于ppt是全英文的,而且内容比较难,所以不建议通过ppt异步学习。

老师上课氛围非常好,每次讲完一个点,都要问同学们听懂了没,如果没听懂可以马上问(可能因为今年是在3A的小教室,所以大家都比较积极地互动,如果改在3C大教室大家可能就会比较腼腆了)

给分也很不错,但是优秀率是有限的,所以老师的给分肯定没法让所有人满意,但是优秀率是给满了的,而且去年优秀率是直接超过了40%,只要认真做了,给分肯定不会差。

我觉得这门课唯一的问题就是ppt不太容易理解。就像我前面说的,ppt是全英文的,而且内容比较难,如果上课认真听了,看着还是比较轻松,但是如果上课摸鱼,自己看的时候会比较痛苦。幸好老师每节课都有录像,如果看不懂还可以自己看录像,建议以后也都把每节课录下来,不然自学真的比较痛苦。

1 0 复制链接
匿名用户 2022春
  • 课程难度:困难
  • 作业多少:很多
  • 给分好坏:杀手
  • 收获大小:没有
  • 难度:困难
  • 作业:很多
  • 给分:杀手
  • 收获:没有

出生(nmd pksq 非要凑10个字是吧)

0 1 复制链接
流术你是什么品种的逆天
立即登录,说说你的看法
账户已注销 2022春
  • 课程难度:中等
  • 作业多少:中等
  • 给分好坏:一般
  • 收获大小:很多
  • 难度:中等
  • 作业:中等
  • 给分:一般
  • 收获:很多

这门课给我的收获还是很大的,让我对形式化的理论和应用有了初步的认知。课程的优点说得挺多了,我说些其他的感受:

  • 大作业的评价方式似乎有些主观,可能无法让所有同学都满意。
  • 上课总体来说是很不错的,不过有时候可能会过于纠结某些细节。
  • 课程安排有待进一步的优化(前半部分节奏略慢)。

最后被卡绩了

0 0 复制链接
匿名用户 2022春
  • 课程难度:困难
  • 作业多少:很少
  • 给分好坏:超好
  • 收获大小:一般
  • 难度:困难
  • 作业:很少
  • 给分:超好
  • 收获:一般

很好的课,可惜我太菜听的不是很懂,后期基本没咋听。这门课没有考试,只有平时作业和大作业,我挑了一个最简单的大作业,不到一天做完就交上去了,最后总评3.0,很感动。

0 0 复制链接

熊焰

教师主页: 戳这里

黄文超

教师主页: 戳这里

解围

教师主页: 戳这里

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

黄文超 10.0 (7) 2021春
熊焰, 黄文超 7.4 (12) 2024春 2023春...

熊焰老师的其他课

操作系统 7.8 (5) 2020秋 2019秋...
形式化方法导引 7.4 (12) 2024春 2023春...
高级操作系统 4.7 (10) 2024春 2023春...
操作系统 2015秋 2012秋...
操作系统原理与设计 2013春 2010秋...
移动互连网计算及安全 2004秋 2003秋...
计算机导论 2007秋
计算机网络 2006春

黄文超老师的其他课

形式语言与计算复杂性 9.6 (15) 2024春 2023春...
形式化方法导引 10.0 (7) 2021春
操作系统 7.8 (5) 2020秋 2019秋...
形式化方法导引 7.4 (12) 2024春 2023春...
现代密码学理论与实践 4.6 (14) 2023秋 2022秋...
操作系统 2017秋

解围老师的其他课

计算机数学 7.0 (3) 2024春 2023春...