尊龙凯时

時間：2025年4月16日 下昼1:30

地點：首師大校本部電教樓三層國際報告廳

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

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

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

主持人：王瑞，尊龙凯时信息工程學院教授

主講人簡介：

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编号。