时间：2025年4月16日 下午1:30

地点：首师大校本部电教楼三层国际报告厅

主讲人：1. 孙猛，北京大学数学科学学院教授，博导

2. 蔡少伟，中国科学院软件研究所研究员，博导

3. 时清凯，南京大学计算机学院副教授，博导

主持人：王瑞，新葡的京集团8814vip信息工程学院教授

主讲人简介：

1. 孙猛，北京大学数学科学学院信息与计算科学系教授，博士生导师， CCF形式化方法专委执行委员，CCF区块链专委执行委员，CSIAM区块链专委常务委员，CSIAM金融科技与算法专委常务委员，CAAI人工智能逻辑专委委员。主要研究领域包括程序理论、软件形式化方法、信息物理系统、深度学习、区块链与智能合约，主持及作为主要成员参与国家自然科学基金、重点研发计划等国家及省部级项目十余项，在TSE、TDSC、ICSE、FSE、FM 、NeurIPS、AAAI等期刊及会议发表论文百余篇，获TASE2015、SBMF2017等国际会议最佳论文奖，曾任ICFEM(2024、2018)、TASE(2023)、FACS(2009、2024)等国际会议程序委员会主席及FM、TACAS等多个国际会议程序委员会委员。

2. 蔡少伟，中国科学院软件研究所研究员，博导，中国科学院优秀导师，CCF杰出会员和杰出演讲者，智源青年科学家，承担多个国家项目和课题，多次获得约束求解领域国际比赛冠军，在领域顶级会议SAT、CP、CAV等获得最佳论文奖/杰出论文奖。成果应用于华为的EDA和操作系统项目，以及多家EDA企业，香山处理器缓存验证，微软云平台故障检测，以及多家互联网头部企业。带领团队研发了首个基于大模型技术的SAT求解器。

3. 时清凯，南京大学计算机学院副教授，博士生导师，国家级高层次青年人才，2020 年于香港科技大学获得博士学位，曾任源伞科技联合创始人、蚂蚁集团技术专家、美国普渡大学博士后研究员。目前主要从事软件分析及软件安全技术研究，其研究成果广泛发表于程序语言（如PLDI，OOPSLA）、软件工程（如ICSE，ESEC/FSE）、网络安全（如SP，CCS）等CCF A 类会议或期刊，曾获ACM SIGSOFT 杰出论文奖、ACM SIGPLAN 杰出论文奖、Google 论文奖、Hong Kong PhD Fellowship。其研究成果广泛应用于诸如阿里、华为等高新技术企业，已帮助企业识别数百个高危漏洞。

主讲内容简介：

1. 报告题目：基于统计模型检查的深度神经网络鲁棒性估计

摘要：以深度神经网络为代表的深度学习系统已在自动驾驶、医疗诊断等安全攸关领域得到了广泛应用。与传统软件系统不同，其数据驱动的特点使得该类系统拥有与传统系统完全不同的决策逻辑，并且深度学习系统的高维输入、庞大参数规模和状态空间使得其复杂程度远远超过传统的软件系统，从而使得目前应用于传统软件系统的形式化技术难以直接应用于大规模深度学习系统的安全性、鲁棒性保障之中。本次报告中将介绍我们近期关于统计模型检查算法改进和深度神经网络鲁棒性估计的部分工作结果。我们对主流统计模型检查工具中使用的Okamoto bound估计方法进行了改进，设计了新的统计模型检查算法，大幅减少了采样次数，可比现有统计模型检查算法节省40%-60%的时间。从统计模型检查的角度，我们给出了深度神经网络鲁棒性的估计算法，仅用少量图片即可获得与传统方法使用大量图片计算得到的全局鲁棒性值强相关的结果。

2. 报告题目：约束求解与EDA形式化验证

摘要：“约束求解”一般是指一种方法论，强调对问题通过某种数学语言进行形式化表达，然后对其进行求解，是计算机解决问题的一种常见方法论。约束求解器，特别是逻辑公式可满足性问题的求解器，包括SAT求解器和SMT求解器，是软硬件验证与测试的基础引擎。约束求解器的性能是许多形式化验证工具性能的关键因素。本报告首先介绍SAT问题和SMT问题的基础内容，然后介绍约束求解的前沿技术，最后介绍相关的EDA形式化验证技术与应用。

3. 报告题目：网络协议安全分析中的形式化方法

摘要：网络协议定义计算机系统如何相互连接，是“人机物”融合时代保障“人机物”互融互通的关键组件，因此，网络协议漏洞可能造成灾难性严重后果。网络协议的形式化规约是各种自动化网络安全分析（如模糊测试、网络监听、模型检测等）的基础，因此格外重要。该报告将介绍网络协议形式化规约推导、生成技术以及其中所包含的形式化方法，其主要思路为通过静态程序分析乃至大语言模型等手段，分析网络协议的实现或文档，构建包含精确语法结构和语义的网络协议规约，并使用构建的精确规约指导下游网络安全分析。截止目前，该工作已找到50余个网络协议中的严重漏洞，包括缓冲区溢出、整数溢出等，并获得10余个CVE编号。