6月28日，由我校科技处、党委组织部、科协主办，信息科学与技术学院（软件学院）承办的“西北大学创新论坛”第一千二百五十五讲暨“弘扬爱国奋斗精神、建功立业新时代”系列活动在长安校区举行。卜磊应邀来校为师生做了题为“基于路径空间遍历的有界验证途径及其应用”的报告。我校相关专业师生代表参加了报告会。

报告首先对大规模复杂软件的可信保障的需求与挑战进行了介绍。说明在工业场景下很多需求都无法满足，需要在系统设计模型和代码层面进行形式化验证。问题逐步从全局验证到有界验证进行过度。指明核心问题为：可达性检验问题全局不可判定。之后阐明了有界验证是软件模型检验通向工业应用的一个可行之路。指明了有界验证的难点与挑战，例如：状态空间爆炸、约束求解能力难以支持、软件代码上难以处理过千行的代码等。卜磊团队独辟蹊径提出了：基于路径遍历的有界验证途径。

之后介绍了由上述思路产生的BACH-BRICK工具，以及该工具在比赛和实际应用中的效果。然后介绍了基于路径验证的复杂系统运行时监控，展示了其在软件代码（C、JAVA、RUST、Solidity）、实时系统（列控、航天、工控、智能驾驶等）、IoT（工控、只能家具等）、AI（验证加固、对抗样本等）领域所展现的突出潜力。

报告结束后，卜磊与在场师生分享了他丰富科研经历，报告引来全场师生的阵阵掌声。