CCF@U第1238场:CCF形式化方法专委走进首都师范大学-最新动态-中国计算机学会_188体育app官网

CCF@U第1238场:CCF形式化方法专委走进首都师范大学

2025-04-18

收藏本文

4月16日，由中国计算机学会（CCF）主办，CCF形式化方法专业委员会和首都师范大学信息工程学院联合承办的“CCF走进高校（CCF@U第1238场）”活动在首都师范大学顺利举行。

本次活动邀请了北京大学数学科学学院孙猛教授、中国科学院软件研究所蔡少伟研究员，南京大学计算机学院时清凯副教授进行了主题报告。形式化方法专委秘书长吴志林、北京市科学技术研究院副院长施智平、首都师范大学科技处处长唐舜、信息工程学院党委书记师怡爽和信工学院师生共计100余人参与本次活动。报告由首都师范大学信息工程学院王瑞教授主持。

会议开始，唐舜处长代表学校对CCF形式化方法专委学者的到来表示热烈欢迎，并简要介绍了学校的基本情况以及CCF走进高校活动的深远意义。

吴志林秘书长强调在人工智能领域大模型迅猛发展的现在，形式化方法作为确保系统可靠性的核心理论工具，其战略价值愈发凸显。同时也对CCF形式化方法专委的发展历史及其与首都师范大学的合作历史进行简单介绍。

孙猛教授以“基于统计模型检查的深度神经网络鲁棒性估计”为题，针对深度神经网络高维输入、复杂状态空间导致的传统形式化方法失效问题，孙猛教授团队提出改进型统计模型检查算法，通过优化Okamoto边界估计方法，将验证采样次数降低40%-60%，显著提升效率。同时，其创新性提出的深度神经网络鲁棒性估计算法，仅需少量样本即可获得与传统大规模测试强相关的全局鲁棒性评估结果，为复杂智能系统的安全性验证提供了新范式。

蔡少伟研究员围绕“约束求解与EDA形式化验证”展开报告，深入剖析了约束求解作为计算机科学基础方法论的核心价值。报告从SAT求解器的底层逻辑出发，解析了SAT求解器在软硬件验证中的引擎作用并介绍了SAT最新算法突破，接着重点介绍了电子设计自动化（EDA）形式化方法的并行求解算法及其在RISC V处理器验证中的实际应用。

时清凯副教授以“网络协议安全分析中的形式化与非形式化方法”为主题，揭示了网络协议形式化规约对“人机物”融合时代的战略意义。针对协议漏洞可能引发的系统性风险，团队创新性地融合静态程序分析与大语言模型技术，实现了从协议文档到精确语法语义规约的自动化生成，并基于此构建了漏洞检测框架。该技术已成功发现50余个高危漏洞，其中10项获CVE国际漏洞认证，为工业互联网、物联网等场景的协议安全分析提供了理论支撑与实践范例。

最后，施智平教授对整个报告做出总结。他指出三位学者的报告从算法创新、工具链升级到产业应用，全景式展现了形式化方法在智能信息系统中的前沿探索，为人工智能可信化发展提供了关键技术路径。同时，他强调形式化方法在各安全攸关领域都有着不可或缺的重要作用，呼吁青年学者深化形式化验证理论学习。

本次CCF形式化方法专委走进首都师范大学的活动气氛热烈、讲者与听众互动充分，通过专家学者与首都师范大学信息工程学院师生的直接对话，为他们带来了创新思维视角，拓宽了他们的学术视野，激发了他们对形式化方法的浓厚兴趣。

收藏本文

<<< 上一篇 CCF@U第1249场：CCF网络与数据通信专委走进中

CCF@U第1240场：CCF理论计算机科学专委与CCF 下一篇 >>>

<<< 下一篇 CCF@U第1240场：CCF理论计算机科学专委与CCF

188体育app官网_188体育投注

CCF@U第1238场:CCF形式化方法专委走进首都师范大学

推荐内容