时间：11月24日19:30-20:30

地点：腾讯会议：553-557-161

主讲人：张文辉 中国科学院软件研究所研究员

主持人： 王瑞 教授

主办单位：信息工程学院

主讲人简介：

张文辉，中国科学院软件研究所研究员、中国科学院大学岗位教授。主要研究兴趣包括形式模型、数理逻辑与程序逻辑、程序性质的推理与模型检测、计算机软件正确性的理论与方法，具体工作包括基于限界正确性检查和不动点算法的检查离散迁移系统CTL性质的模型检测工具VERDS的相关理论研究与算法实现。

主讲内容简介：

正确性是计算机理论和应用中的重要问题。对于很多类型的软件系统的时序性质，其正确性是基于系统的无限运行进行定义的。这样的正确性定义难以直接用于验证。限界正确性是一种定义在有穷路径上的正确性，为正确性的验证提供了一种手段。本报告围绕正确性和限界正确性介绍这些概念之间的关系并介绍限界正确性检查作为一种验证正确性的手段的相关技术及其和传统基于不动点计算的符号模型检测方法的比较。