2026年9月18日，CCF@U第1475场——CCF形式化方法专业委员会走进贵州大学特邀报告会在贵州大学博学楼13楼报告厅成功召开。本次活动由中国计算机学会（CCF）主办，CCF形式化方法专业委员会与贵州大学联合举办。国家特聘专家、西南大学教授、博士生导师、软件理论与系统团队负责人、软件研究与创新中心（RISE）主任刘志明，华东师范大学软件工程学院教授、院长助理、博士生导师李钦，南京大学计算机学院副教授、博士生导师、国家级青年人才时清凯，中国科学院软件研究所基础软件与系统重点实验室研究员、常务副主任吴志林，以及包括黄瑞章教授、王以松教授在内的贵州大学师生代表齐聚现场，围绕可信软件与系统、神经符号协同、形式化验证、处理器设计形式化验证、软件栈测试等前沿领域展开深度学术交流。

首先，贵州大学计算机科学与技术学院党委书记龙慧云副教授致欢迎词。她对CCF形式化方法专业委员会专家团队的到访表示热烈欢迎，简要介绍了学院的学科布局、科研发展及人才培养情况，并希望以本次学术交流为契机，深化校企院所间的科研合作，助推学院相关专业实现高质量发展。本次报告会由贵州大学计算机科学与技术学院副院长黄瑞章教授与贵州大学人工智能研究院院长王以松教授共同主持。

龙慧云书记致欢迎词

全体与会人员合影

刘志明教授作了题为《谈人工智能时代的可信软件与系统》的报告。报告首先介绍了可信软件与系统的基本概念，回顾了第一次软件危机及软件工程的发展历程，阐述了软件抽象与形式化方法如何支撑软件应用领域的持续拓展，应对软件系统规模和复杂度的不断增长，并推动软件可信性的持续提升。报告进一步指出，随着人工智能逐渐成为软件系统的重要架构成分，并深度参与软件全生命周期，生成式AI与智能体AI正在引发一场以“软件与系统的可信性危机、从业人员的信心与职业价值危机，以及AI能力与影响的多重悖论”为基本特征的第二次软件危机。在此基础上，报告探讨了可信智能软件与系统工程的内涵、外延及其面临的主要挑战，并展望了人工智能时代可信软件与系统研究和人才培养的新问题、新方向与新机遇。

刘志明教授作特邀报告

李钦教授作了题为《神经符号协同的智能化软件工程质量保障技术》的报告。他指出，自大语言模型（LLM）问世以来，软件工程领域迎来了重要变革，在软件开发过程中引入大模型和大模型智能体生成软件制品已逐渐成为主流开发模式。然而，围绕大模型安全与可信的挑战始终存在，如模型幻觉、逻辑推理能力薄弱、数据与模型隐私安全及公平性等问题日益突出，数据质量保障、模型决策正确性验证、数据驱动的软件制品与传统逻辑驱动的软件制品融合与协同等系统性挑战，制约了智能化技术在软件工程领域的深度应用。在此背景下，他聚焦神经模型与符号模型的交叉协同，为推动智能技术在软件工程领域从“可用”走向“可信”提供了重要洞察与思考，并介绍了课题组近期在该领域的相关进展。

李钦教授作特邀报告

时清凯副教授作了题为《面向网络协议软件栈的测试预言问题探索》的报告。他以“无规约，无可测；有规约，难可信”这一网络协议测试中预言机问题的本质循环困境为切入点，介绍了课题组在这一循环中的三类实践：从实现中学习规约、从文档中学习规约，以及绕过规约学习一致性关系。这三类实践分别对应“规约缺失”“规约不可信”“规约不可得”三种现实场景。报告还以主流网络协议上的实验为例，分享了对每种方法的思考。

时清凯副教授作特邀报告

吴志林研究员作了题为《RISC-V处理器设计形式化验证》的报告。他围绕中国科学院软件研究所基础软件验证研究室近年来在RISC-V处理器设计形式化验证方面的工作展开介绍，涵盖模型检测基础引擎、RISC-V处理器指令集一致性验证、算术电路验证等内容，并对未来工作进行了展望。

吴志林研究员作特邀报告

在自由交流研讨环节，现场师生围绕可信软件与形式化方法、软件工程质量、网络协议测试、处理器设计形式化验证等问题踊跃提问，与会专家逐一细致解答，并从课题申报、本科生科研启蒙、研究生培养方案等方面给出建设性指导意见，现场学术研讨氛围十分热烈。

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

特邀专家和部分师生合影留念