轩宇信息诚邀您参加2026CCF中国软件大会智能化高可信嵌入式工程技术论坛

嵌入式软件在航天、航空、轨交、汽车、核能等领域广泛应用，是重大装备关键功能的主要实现载体。随着人工智能技术的飞速发展，嵌入式软件开发测试方法正发生深刻的变革。一方面，嵌入式软件自身正在成为人工智能的实现载体，另一方面，智能化软件工程新方法也成为高可信、高效率研制嵌入式软件的重要支撑。

本论坛由航天科技集团502所高可信嵌入式软件工程专业实验室和北京轩宇信息技术有限公司发起，旨在加强工业需求和学术前沿融合，为工业界现实问题凝练和学术界成果更好服务国家重大需求架起桥梁，至今已在CCF ChinaSoft 举办 6 届，致力于成为学术界和工业界探讨可信嵌入式软件的交流平台。

本届论坛聚焦智能化高可信嵌入式软件开发、测试方向，将邀请来自工业界和学术界的多位专家在相关方向共同探讨工业界挑战和学术研究前沿。

论坛组织委员会

• 顾斌（航天科技集团502所，北京轩宇信息技术有限公司）

• 陈睿（航天科技集团502所，北京轩宇信息技术有限公司）

• 李晓锋（航天科技集团502所）

论坛安排

日程安排：

时间：2026年11月8日，09:00-12:00

地点：天津市社会山国际会议中心酒店，二层18号会议室

论坛议程：

论坛报告嘉宾简介

题目：面向程序分析与验证的约束求解

摘要：约束求解是人工智能领域的经典问题，也是多种程序分析与验证方法的底层支撑，约束求解的能力和效率直接影响分析验证的效果。本报告将介绍课题组近期在面向程序分析与验证的约束求解方面开展的工作，希望以融合增强、白盒使用、场景定制等思路来提升程序分析与验证背景下约束求解的能力和效率，具体分享该思路在符号执行、别名分析、未解释函数程序验证等典型场景下取得的进展。

简介：陈振邦，国防科技大学计算机学院教授、博士生导师，2025年入选教育部国家级人才奖励计划。主要研究方向为形式化方法、程序分析与验证、程序综合及其在不同背景下的应用。近年来主要围绕符号执行相关的理论、技术和应用开展研究，成果发表在OOPSLA、FM、ICSE、FSE、ISSTA、ASE、TOSEM等重要国际会议或期刊上，获ACM SIGSOFT杰出论文奖4次。获国家科技进步二等奖1项、军事科学技术进步一等奖1项、省部级二等奖2项，获NASAC青年软件创新奖。

题目：自动驾驶系统仿真测试探索

摘要：本报告结合团队近年来在自动驾驶仿真测试与质量保障方面的工作，以多个端到端和模块化的开源自动驾驶系统作为被测对象，围绕仿真场景的评估和生成技术展开讨论，分享如何利用仿真反馈主动探索风险，借助大语言模型将历史事故报告转化为可复用的风险事件，以及通过真实驾驶数据与世界模型生成兼具真实性和挑战性的测试场景。同时，围绕场景覆盖、违规判定与评估一致性，探讨如何在有限的测试资源下更有效地发现自动驾驶系统中的潜在安全问题。

简介：周宇，南京航空航天大学计算机学院教授、博导，主要研究领域为智能化软件技术、新型测试技术等，CCF系统软件专委会/软件工程专委会/开源发展委员会执委，江苏省信息技术应用学会常务理事，江苏省计算机学会软件专委会副主任，“高安全系统的软件开发与验证技术”工信部重点实验室副主任，在国内外重要期刊和会议上如IEEE TSE、ACM TOSEM、ICSE、FSE、ASE、《中国科学》，《软件学报》等发表论文100余篇，授权国家发明专利20余项，出版专著3部，担任Journal of Software: Evolution and Process、《计算机科学》等国内外期刊编委，科研成果获得中国指控学会“科技进步奖”二等奖1项、中电联“电力创新奖”一等奖1项，教学成果获得江苏省教学成果二等奖1项。

题目：智能体驱动的大规模程序验证

摘要：大规模软硬件系统的全自动验证是形式化方法领域的“圣杯”问题。传统的演绎验证借助模块化契约推理可扩展至大型系统，但其核心瓶颈在于形式规约的构造——该环节长期依赖专家人工，是工业级验证应用的主要成本来源。本报告介绍我们近期利用大语言模型与智能体技术推动规约自动合成、进而实现大规模程序（无运行时错误）自动验证的两项工作。其一，大语言模型驱动的细粒度形式规约生成与精化框架Preguss，通过潜在运行时错误引导规约生成过程，在静态分析与演绎验证之间建立高效协同，首次实现了对千行级真实C程序的几乎完全自动化验证；其二，多智能体并行模块化验证框架Verdict，通过基于假设契约的并行规约合成与双向跨过程冲突消解机制，突破传统自底向上验证范式的可扩展性瓶颈，首次在数小时内完成对两万行级X.509证书解析器的几乎完全自动化验证——此前该任务需数月的专家人工投入。上述结果表明，智能体驱动的模块化规约合成为大规模程序的自动化验证提供了一条切实可行的路径。

简介：陈明帅，浙江大学研究员、博士生导师、启真学者，CCF形式化方法专委执行委员、系统软件专委通讯委员，国家优秀青年基金（海外）获得者。2019年于中国科学院软件研究所获计算机软件与理论专业博士学位，此后于德国RWTH Aachen从事为期3年的博士后研究工作，2023年初加入浙江大学。主要研究方向包括形式验证、程序理论、概率系统、信息物理融合系统、AI4FM等，与合作者一起，提出新型安全攸关系统形式验证理论，解决了概率程序不动点估计、微分系统可达性判定、时滞系统高效控制生成等若干软件理论难题，研究成果应用于我国月球探测和卫星姿轨控制等重大工程，在Inf. Comput.、CAV、FM、OOPSLA、TACAS等领域旗舰期刊/会议上发表学术论文50余篇，曾获中科院院长特别奖、ATVA杰出论文奖、FMAC最佳论文奖。

题目：可信软件工程的左右脑：需求智能体与测试智能体

摘要：本报告聚焦智能体驱动的软件工程，围绕前端需求分析与后端测试生成展开。在前端，智能体实现需求对齐、澄清与质量提升，为代码生成提供精确输入；在后端，通过基于代码的测试增强、代码与需求一致性校验及基于需求的黑盒测试，保障代码质量。研究展示了该范式通过需求理解与测试验证的前后端协同，在提升开发效率、降低缺陷率方面的成效，并讨论了挑战与发展方向。

简介：陈俊洁，天津大学教授、博导、软件学院副院长，软件工程团队(TJU-WISE Lab)负责人，主持国家优青、重点研发计划青年科学家等项目；博士毕业于北京大学；研究方向主要为基础软件质量保障、代码智能体等；入选中国科协青年人才托举工程、斯坦福大学发布的全球前2%顶尖科学家榜单，荣获CCF优博、电子学会自然科学一等奖、十余项最佳/杰出论文奖等奖项；成果在华为、字节等多家知名企业落地；担任AUSE、FCS、JCST、JSEP等期刊编委/青年编委，ICSE、FSE、ASE、ISSTA等顶会PC。

题目：低资源场景下大模型赋能的代码安全智能审计

摘要：面对AI编程时代软件迭代加速、安全漏洞剧增且损失惨重的严峻形势，静态分析作为安全左移的核心手段，因复杂语义鸿沟与漏洞模式爆炸陷入高误报漏报瓶颈，而智能体分析又面临成本与可靠性挑战。为此，我们提出AI增强的分析引擎与自动运维规则库的双重驱动方案：一方面，利用大模型推断跨语言调用与动态特性等复杂语义，融合进静态分析流水线提升分析精度；另一方面，基于千万级开源代码自动挖掘漏洞变种、检验规则并生成优化补丁，实现规则库自进化。实验表明，引擎在跨语言分析数据集上较基线提升30%，成功检出27个真实跨语言漏洞中的16个；规则库累计生成千余条检测规则并优化200余条，自动化运维质量可以媲美专家。相关研究成果已发表于USENIX Security、CCS、ASE等顶会。

简介：文明，华中科技大学教授，博士生导师，“华中学者”卓越青年学者，博士毕业于香港科技大学，主要聚焦系统软件安全、大模型智能体等相关研究，在SOSP、CCS、OOPSLA、ASPLOS、ICSE、FSE等国际会议上累计发表了CCF-A类高水平论文70余篇，多次获得ACM SIGSOFT杰出论文奖。出版《软件安全》、《编译原理》等著作多部，主持/参与国家重点研发计划、国家自然科学基金青年项目(B类，C类)、面上项目、国家自然科学基金通用联合重点项目、湖北省重大攻关项目课题、CCF华为胡杨林基金等项目，授权/申请国家发明专利10余项，入选第七届中国科协青年人才托举工程计划。

题目：面向空间飞行器控制算法的可信代码智能生成

摘要：大语言模型的出现深刻改变了软件开发方式，借助大模型和编程智能体自动生成代码正逐渐成为主流开发模式。然而在航天等安全攸关领域，控制算法需求以数学公式与伪代码为主要表达形式，控制逻辑与工程约束高度耦合，通用大模型缺乏领域知识，生成代码易出现与需求逻辑不一致、虚构底层函数、违反编程规范等问题。同时，研制数据不能出域，无法直接使用外部商业大模型；编译、静态分析等常规检查只能判定代码的语法与规范符合性，难以判定生成代码与需求算法是否逻辑等价，生成结果仍需人工逐行比对确认。这些都制约了大模型在高可靠软件研制中的深度应用。在此背景下，本报告聚焦大模型代码生成从“能用”走向“可信”，介绍团队在领域大模型数据构建与训练微调、神经符号融合的可信代码生成、验证反馈驱动的端到端生成与闭环修正等方面的研究进展。

简介：杨逸，博士，北京控制工程研究所软件中心工程师，毕业于北京理工大学计算机科学与技术专业。主要研究方向为智能软件工程、可信代码生成与软件验证等。参与国家自然科学基金重大项目、科技创新2030“新一代人工智能”重大项目、国家重点研发计划项目等科研工作，相关成果发表于 ICDE、VLDB 等国际会议和期刊。

论坛组织委员会简介

简介：顾斌，航天科技集团 502 所研究员，博士生导师。主要研究方向为航天器控制、可信软件、软件智能化开发和形式化方法等。

简介：陈睿，博士，航天科技集团502所研究员，轩宇信息董事长，CCF形式化方法专委会常务委员，CICC智能测评专委会委员。长期从事嵌入式软件可信保障技术以及相关工具软件的研制。主持多个国家级省部级项目，在ISSTA、FSE等发表高水平论文20余篇，获发明专利20余项。负责研制了覆盖嵌入式软件测试全过程的完整工具链，推动软件工程和形式化等技术产业化，广泛应用于载人飞船和空间站、嫦娥系列探测器、北斗导航卫星等航天器软件的开发和测试中。入选首都科技创新领军人才，获北京市杰出青年中关村奖、北京市科技进步一等奖，航天贡献奖等。

简介：李晓锋，研究员，现任中国空间技术研究院软件技术专业学术技术带头人、北京控制工程研究所软件中心主任，兼任航天科技集团软件专业组成员、CCF软件工程专委会执行委员、CCF 嵌入式系统专委会执行委员。长期从事航天器高可信嵌入式软件领域的科学研究与工程实践，具有深厚的理论基础和丰富的型号研制经验。作为项目负责人，主持完成了嫦娥系列探测器、星网星座等十余项国家重大航天工程型号嵌入式控制软件的研制任务；先后主持或参与核高基重大专项、国防基础科研预研、国家自然科学基金等国家级科研项目二十余项。主要研究方向涵盖可信软件、软件自动化、软件自适应演化等前沿领域。曾获北京市科学技术进步一等奖、军队科技进步奖、国际发明展览会金奖等多项重要奖励；累计发表学术论文五十余篇，获授权发明专利四十余项。