报告题目：基于路径空间遍历的有界验证途径及其应用

报告人：卜磊 教授  南京大学

报告时间：2021年3月9日 14:00

报告地点：理科大楼B1002

报告摘要：人类社会正在进入软件定义一切的时代，软件系统的规模和复杂性增长进一步加剧，软件可信保障面临更加严峻的挑战。复杂软件系统中连续与离散行为交织、状态空间爆炸、非线性行为难以建模等障碍使得系统验证过程中的复杂性难以控制，现有方法与技术离处理实际问题需要存在较大差距。本报告系统地阐述我们为有效解决复杂系统验证过程中的复杂性控制问题所提出的基于路径空间遍历的有界验证途径。我们从单条路径状态空间验证出发控制整体验证的复杂性；通过路径中不可行片段的抽取进行路径空间缩减；设计新型浅同步语义规避组合状态空间爆炸；引入智能化动态迭代求解技术处理非线性约束难解问题；在此基础上，我们进一步将相关技术拓展至面向场景的复杂软件系统在线验证与控制生成，对软件系统行为可靠性进行系统性保障。基于上述工作，我们开发了复杂软件系统模型检验工具集BACH。与国际上同类相关工具相比，BACH在基准案例集上的性能明显超出，获得广泛关注与影响，并在列控、航天、物联网等领域得到实际应用验证。 

报告人简介：卜磊，南京大学计算机科学与技术系教授，博士生导师；2010年在南京大学获取计算机博士学位；曾在CMU、MSRA、UTD等科研机构进行访学与合作研究；主要研究领域涉及软件工程、可信软件、形式化方法，研究工作集中在模型检验技术、实时混成系统、信息物理融合系统等方面，部分创新性工作发表在相关领域重要期刊与会议如《中国科学》、TCAD、TC、TCPS、TPDS、RTSS、CAV等上；入选高校计算机专业优秀教师奖励计划、中国计算机学会青年人才发展计划、微软亚洲研究院铸星计划, 获NASAC青年软件创新奖等。