2020年9月30日上午，西南交通大学数学学院吴贯锋博士应学院邀请在河南省大数据分析与处理省重点实验室（曾宪梓楼）一楼会议室，做了主题为“形式化验证技术的研究和应用简介”的学术报告。报告会采取了线下线上相结合的方式进行，计算机与信息工程学院和实验室的部分师生到现场参加了报告会，报告由刘扬博士主持。

报告会上，吴贯锋博士详细讲解了形式化验证技术的研究和应用，在报告中讲出测试、仿真和形式化方法是目前在高安全领域中保证系统正确性的主要手段，仿真与测试是比较常见的方法，因其处于软件开发周期的下游，针对的是已完成的系统，这使得其只能发现错误，而不能证明系统完全没有错误。而形式化验证技术是基于数学推理的方法证明系统无错误。简单来说，就是建立数学模型，采用逻辑符号描述系统的行为，将系统行为形式化为逻辑公式，通过对逻辑公式的可满足性判定，证明系统无错误。在软件验证方面，相比于传统软件测试方法，形式化方法不插桩、不需要测试例，能够以静态方式发现程序中的运行时错误，可证明在一定的条件下系统无错误。形式化方法是NASA保障其软件安全可靠的重要手段，在航空航天、轨道交通等安全苛求领域对形式化方法的应用已纳入了相关的行业标准中。报告在师生们热烈的掌声中结束。

吴贯锋，男，本硕就读于河南大学计算机与信息工程学院，2014进入西南交通大学信息学院攻读博士学位，2019年毕业留校工作。主要研究方向为自动推理、形式化验证、并行计算。近5年，以一作和通讯作者发表期刊和会议论文近10篇，主研中央军委科技委H863项目1项，省部级项目1项，国家自然科学基金项目2项，企业横向课题2项。主持校级项目2项。2018年国际SAT问题竞赛亚军。