首页·交流合作
实验室举办主题为“软件正确性与形式验证”的学术讲座
发布时间:2018-04-29

4月28日,在工科大楼A座5楼会议室,重点实验室邀请中科院软件所计算机科学国家重点实验室研究员、中国科学院大学教授张文辉为师生做了一场主题为“软件正确性与形式验证”的学术讲座,讲座由计算机科学系徐戈副教授主持。

讲座中,张文辉教授先以“软件在尖端领域的广泛应用”为切入点引出话题,认为软件可靠性是一个非常重要的问题。接着,他提到形式化方法是提高软件系统,特别是Safety-Critical系统的安全性与可靠性的重要手段,并验证分析了软件系统是否满足给定性质的模型检测法。他还介绍了限界语义与限界正确性检查的基本思想以及关于计算树逻辑CTL性质的限界正确性检查的一些重要进展,并论述形式验证的主要方法的应用实例以及工具说明模型检测方法的应用。

在互动环节中,老师和同学们踊跃发言,张教授一一做出详细的解答。最后,讲座在热烈的掌声中落下了帷幕。

张文辉教授.png

【背景链接】

张文辉,中科院软件所计算机科学国家重点实验室研究员,2000年入选中国科学院百人计划。多年来致力于计算机软件正确性的理论与方法、形成模型、推理与模型检测、数理逻辑与程序逻辑的研究,实现了基于限界正确性检查和基于不动点算法的检查离散迁移系统CTL性质的模型检测工具VERDS。