汇报内容

1、提问形式化验证的方向：
（1）定理证明器：将主流算法等用形式化语言编写，并加以证明。
（2）模型检测：将主流系统或算法进行建模，使用建模工具进行验证，可判定问题、完备性。
2、目标和方向
3、如何寻找形式化方向的论文，书本看的选择
4、本周主要是学习课程，在进程代数和系统分析与验证中，对KS建模，一阶谓词逻辑等进行学习

导师反馈内容

1、软件工程的需求，形式化验证是实现需求，用数学语言定义需求等。在形式化中，越来越多的工业软件在使用，除了航空航天，还有自动驾驶、轨道交通等。
2、可信方面上数学主要是以统计和优化为主。
3、人工智能的可解释性可以从：X-AI（explain AI）
4、形式化验证文章：CAV/TACAS/FSE ｜ICSE/ICFEM｜FAC/理论计算机科学
5、计算机逻辑基础的某一章讲述的CTL是Model Checking；Model Checking书较为简单；principle of Model Checking理论、数学较强，较难理解。
6、Formal method和程序理论配合着看。
7、对于书进行解释，需要用自己的语言进行组织来阐述。