题目：互补近似可达验证技术及其应用研究

主讲人：华东师范大学研究员，博导李建文

时间：2022年1月13日（星期四）上午10:00

腾讯会议号： 497-586-328

欢迎全校师生积极参加！

摘要：互补近似可达验证（简称CAR）是报告人近年来在形式化验证领域提出并主要研究的一种新型安全模型检查技术（safety model checking）。该技术和主流的IC3/PDR验证技术相比，具有更加清晰的理论框架和灵活的状态搜索策略。在给定测试集中CAR的性能和IC3/PDR相比也有很强的竞争力。本报告首先会简要介绍一个CAR的方法学和它的最新进展，之后会汇报CAR在轨道交通连锁系统验证和芯片设计验证领域中的初步应用结果。最后简要探讨形式化验证技术，尤其是模型检查技术在工业界应用前景的一些想法。

主讲人简介：李建文，华东师范大学研究员，博士生导师，入选上海市青年人才计划，获得上海市浦江人才荣誉称号，主持国家自然科学基金青年项目、重点项目子课题各一项。研究方向主要为形式化自动验证技术，可用于保障计算机软硬件系统的正确性和安全性，重点应用场景包括芯片、航天、轨道交通等安全攸关领域