2024春 2023秋 2023春 2022秋 2022春 2021秋 2021春 2020秋 课程号：EIEN7002P02
- 课程难度：中等
- 作业多少：中等
- 给分好坏：超好
- 收获大小：很多
| 选课类别：基础 | 教学类型：理论课 |
| 课程类别：研究生课程 | 开课单位：软件学院苏州 |
| 课程层次：博士 | 学分：3.0 |
形式化方法是计算机科学理论中历史最悠久也最高度发达的学科，该学科最早起源于数理逻辑和数学基础的研究，主要关注形式系统建模、语义学和可满足性等理论问题；同时，该学科和计算机软件理论研究深入交叉融合，在软件系统建模与软件可靠性证明、Hoare逻辑系统、程序合成、程序切片、符号执行等研究领域都有重要应用。尤其在最近十多年来，随着大数据、云计算、区块链等技术的发展，形式化方法技术在一键式证明、云服务安全架构、智能合约证明等领域也都得到了广泛应用。
本课程对在计算机科学中广泛应用的形式化方法理论和典型应用做全面的介绍，基本内容包括形式化方法的基础知识、命题逻辑、布尔可满足性、一阶逻辑、可满足性模理论、等式与未解释函数、线性算术理论、数据结构相关理论、理论组合、软件形式化建模、符号执行、程序验证、程序合成、程序切片等。
通过本课程的学习，学生将能够理解形式化方法的理论内容和体系，了解最新的研究趋势和研究进展，锻炼培养形式化能力和创新能力，为后续学习其它进阶课程打下坚实基础。
- 课程难度：中等
- 作业多少：很多
- 给分好坏：一般
- 收获大小：很多
- 难度：中等
- 作业：很多
- 给分：一般
- 收获：很多
一句话评价:华保健老师，软院里唯一真正意义上能与国际一流大学接轨的老师。
- 课程难度：简单
- 作业多少：很少
- 给分好坏：超好
- 收获大小：很多
- 难度：简单
- 作业：很少
- 给分：超好
- 收获：很多
这门课看着唬人，实际很好过，老师上课讲的很通俗易懂，如果想混的话就认真听习题课，考试的时候打印好习题课的课件带上就行，dpllt 符号执行，混合执行的这些偏后面的不用看，题量大，做不到那里的。23春有8次实验作业，不过有git大爹。 老师给分很高，认识的没有低于80的，附2023春考题（少了几个题，记不起来了。我空了3题，两个证明只写了一半，也80+了，华老师非常值得信任 yyds）： 命题逻辑证明1题 sat一题 EUF 一题 代码和ppt很像，但引入了结构体取值 EUF还问了如何证函数等价（证否命题unsat） LA一题（消元法） 谓词逻辑证明一题 bit vector 给一个表达式，画那个树，标约束 指针一题（3小问，涉及R(x），H1（H2(X）) dpllt一题 混合执行一题（求path condition）其他的记不得了
- 课程难度：困难
- 作业多少：中等
- 给分好坏：超好
- 收获大小：很多
- 难度：困难
- 作业：中等
- 给分：超好
- 收获：很多
bj老师讲课讲的是真的好，能学到很多有趣的东西。这门课主要是从数学的角度去审视程序（从比特向量理论到符号乃至于软件测试），然后学会了些好玩的算法和工具。
但是个人觉得这门课可能对一般的计算机就业（非科研向，尤指前端后台）并无多少帮助，就像是学哲学一样，只是对程序有了一种审视的新角度。但是对于写 compiler 或者想搞 TPL 的同学来说，这个很有帮助。
有书面作业，也有写代码作业（写代码的作业次数更多），基本上一周布置一次作业。
这门课期末考试是开卷的，不适宜突击，因为出题灵活。但是只要平时听课，至少要能独立做出作业，就基本不怎么需要期末突击（因为这门课是真的只要理解原理，就能够应变灵活的题目），最多期末时做做往年试卷大概知道有什么题型，心里有个底。给分很高。
- 课程难度：简单
- 作业多少：很少
- 给分好坏：超好
- 收获大小：很多
- 难度：简单
- 作业：很少
- 给分：超好
- 收获：很多
非常推荐！！！
平时：没有点名，上课时会由数学史入手，来介绍这部分内容在数学中的作用（对于对数学感兴趣的同学非常有意思），认真听讲会有很多收获。然后会讲解在计算机中的实现（通过 python 和 z3工具包），在每节课结尾会带着做实验，代码同样可以 git 。
考试：开卷，题型固定，看22的 review 再结合往年试卷就足以完成所有题目，做完了所有题目，出分95+。
