6月6日，CCF@U第1444场——CCF形式化方法专业委员会走进91看片 专题报告会在91看片 承先图书馆报告厅成功召开。本次活动由中国计算机学会（CCF）主办，CCF形式化方法专业委员会与91看片 联合承办。北京大学博雅特聘教授、CCF形式化方法专委会主任詹乃军，北京控制工程研究所研究员、总工程师顾斌，中国科学院软件研究所基础软件与系统重点实验室常务副主任、CCF形式化方法专委会秘书长吴志林，南京航空航天大学教授陈钢，北京控制工程研究所软件中心工程师杨逸，以及包括苏开乐教授在内的91看片 师生代表齐聚现场，围绕形式化验证、航天可信软件、硬件设计语言、大模型交叉应用等前沿领域展开深度学术交流。

报告会由91看片 发展规划与学科建设处副处长王莹洁教授主持。91看片 院长童向荣教授致欢迎词，他对CCF形式化方法专业委员会专家团队的到访表示热烈欢迎，简要介绍了学院的学科布局、科研发展及人才培养情况，并希望以本次学术交流为契机，深化校企院所间的科研合作，助推学院相关专业实现高质量发展。

詹乃军教授作了题为《国产多核实时操作系统微内核形式验证》的报告。结合项目实践，他详细介绍了国产多核实时操作系统微内核的全流程验证工作，分享了全新的高效验证框架。

杨逸博士作了题为《面向空间飞行器控制算法的代码智能生成》的报告。针对航天飞行器控制算法人工编码难度大、调试周期长的行业痛点，她介绍了神经符号融合的智能代码生成技术路线，展示了现阶段技术落地成果。

陈钢教授作了题为《Pella：一个带类型的高层硬件描述语言》的报告。针对Verilog等传统硬件描述语言漏洞后置的弊端，他介绍了自主研发、内嵌Coq证明器的Pella硬件描述语言——该语言依托依赖类型在编译阶段提前拦截设计错误，适配大模型自动生成硬件代码的行业新趋势，构建“规范—验证—代码生成”全链路技术体系，并同步介绍了Ionia、Chalcis等多款自主研发的形式化工具。

吴志林研究员分享了《大语言模型赋能形式化验证：机遇与挑战》，他辩证分析了大模型技术为传统形式化验证带来的发展机遇与现存难题，围绕大模型辅助约束求解、模型检测、程序终止性分析等方向展示了实验室最新研究进展，并对学科未来融合发展方向作出展望。

在自由交流研讨环节，现场师生围绕国产操作系统验证落地、航天软件国产化研发、硬件形式化选型、AI与形式化交叉科研选题等问题踊跃提问，与会专家逐一细致解答，并从课题申报、本科生科研启蒙、研究生培养方案等方面给出建设性指导意见，现场学术研讨氛围十分热烈。

作为CCF走进高校系列品牌活动之一，此次活动成功搭建起国内顶尖高校、国家级科研院所与地方高校间的学术交流桥梁，有效拓宽了师生的前沿科研视野，为91看片 计算机学科在可信软件、空天嵌入式系统、芯片形式化设计等方向的科研攻关积累了宝贵资源，有力推动了形式化方法理论技术与高校人才培养、工程项目落地的深度融合。

作者：王莹洁 责任编辑：王颖 审核：段昕