报告题目：形式化验证技术的研究和应用
报告人：吴贯锋 博士（西南交通大学）
时间：9月30日上午 10:00-12:00
地点：曾宪梓楼西侧205会议室

测试、仿真和形式化方法是目前在高安全领域中保证系统正确性的主要手段，仿真与测试是比较常见的方法，因其处于软件开发周期的下游，针对的是已完成的系统，这使得其只能发现错误，而不能证明系统完全没有错误。而形式化验证技术是基于数学推理的方法证明系统无错误。简单来说，就是建立数学模型，采用逻辑符号描述系统的行为，将系统行为形式化为逻辑公式，通过对逻辑公式的可满足性判定，证明系统无错误。在软件验证方面，相比于传统软件测试方法，形式化方法不插桩、不需要测试例，能够以静态方式发现程序中的运行时错误，可证明在一定的条件下系统无错误。形式化方法是NASA保障其软件安全可靠的重要手段，在航空航天、轨道交通等安全苛求领域对形式化方法的应用已纳入了相关的行业标准中。
   吴贯锋博士本硕就读于河南大学计算机与信息工程学院，2014进入西南交通大学信息学院攻读博士学位，2019年留校在数学学院系统可信性自动验证国家地方联合工程实验室工作。主要研究方向为自动推理、形式化验证、并行计算。近5年，以一作和通讯作者发表期刊和会议论文近10篇，主研中央军委科技委H863项目1项，省部级项目1项，国家自然科学基金项目2项，企业横向课题2项。主持校级项目2项。2018年国际SAT问题竞赛亚军。
热忱欢迎广大感兴趣的师生积极参与！

主办：河南大学计算机与信息工程学院，河南省大数据分析与处理重点实验室，河南省空间信息处理工程实验室