尊龙凯时

時間：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編號。