尊龙凯时

時間：2023年6月20日（周二）15:00

地點：信息工程學院二層大會議室

主講人：蔔磊

主持人：施智平

主辦單位：信息工程學院

主講人簡介：

卜磊，教授，博士生导师，现任南京大学软件学院副院长，兼任 CCF 系统软件专委秘书长；2010年在南京大学盘算机与科学手艺系获取博士学位；曾在CMU、MSRA等科研机构举行访学与相助研究；主要研究领域涉及软件工程、可信软件、形式化要领，研究事情集中在模子磨练手艺、实时混成系统、信息物理融合系统等方面，部分立异性事情揭晓在相关领域主要期刊与聚会如《中国科学》、TCAD、TC、TDSC、TCPS、TPDS、RTSS、ICSE、ISSTA、ASE等上；入选国家级青年人才妄想、高校盘算机专业优异西席奖励妄想、CCF-IEEE CS青年科学家奖、NASAC青年软件立异奖、CCF青年人才生长妄想、MSRA铸星妄想等。

主講內容簡介：

人类社会正在进入软件界说一切的时代，软件系统的规模和重大性增上进一步加剧，软件可信包管面临越发严肃的挑战。重大软件系统中一连与离散行为交织、状态空间爆炸、非线性行为难以建模等障碍使得系统验证历程中的重大性难以控制，现有要领与手艺离处置惩罚现实问题需要保存较大差别。本报告系统地叙述我们为有用解决重大系统验证历程中的重大性控制问题所提出的基于路径空间遍历的有界验证途径。我们从单条路径状态空间验证出发控制整体验证的重大性；通过路径中不可行片断的抽取举行路径空间缩减；设计新型浅同步语义规避组合状态空间爆炸；引入智能化动态迭代求解手艺处置惩罚非线性约束难明问题；在此基础上，我们进一步将相关手艺拓展至面向场景的重大软件系统在线验证与控制天生，对软件系统行为可靠性举行系统性包管�；�于上述事情，我们开发了重大软件系统模子磨练工具集BACH。与国际上同类相关工具相比，BACH在基准案例集上的性能显着凌驾，获得普遍关注与影响，并在列控、航天、物联网等领域获得现实应用验证。