CCF软件大会2026|优秀博士生激励计划论坛

一、论坛介绍

本论坛为ChinaSoft常设论坛，旨在推动中国计算机领域的科技进步，鼓励创新性研究，激励计算机领域的博士研究生潜心钻研、务实创新，解决计算机领域中需要解决的理论和实际问题，表彰做出优秀成果的年轻学者而设立。论坛面向软件工程、系统软件、形式化方法等领域的优秀博士生，旨在为青年科研人员提供高水平、多方向的学术交流平台，集中展示相关创新研究成果，促进不同研究方向之间的交流与交叉融合。论坛主要通过优秀博士生或青年学者学术报告、专家点评及互动交流等形式开展，已成为ChinaSoft面向优秀青年科研人才的重要交流平台。

二、论坛组织委员会

• 印莹（东北大学）
• 张昕荻（中国科学院软件研究所）
• 李明煜（中国科学院软件研究所）

三、论坛安排

日程安排：

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

地点：天津市社会山国际会议中心酒店，一层2号大宴会厅

论坛议程：

四、论坛报告嘉宾简介

1. 报告人：崔炜皞 博士后研究员

题目：Xtrace：基于二进制指令拼接的高保真 GPU 核内追踪

摘要：随着 GPU 内核日益复杂，传统核内追踪方法容易因探针插入干扰编译优化和运行时调度，导致追踪结果失真。Xtrace 提出二进制级指令拼接技术，在编译后直接插入探针，并结合寄存器活跃性分析与冒险感知调度降低运行扰动。Xtrace 支持 NVIDIA 和 AMD 共 19 种 GPU 架构，可保持 94–98% 的原始指令，并以较低开销实现高保真追踪，为 GPU 性能分析和智能体驱动的自动优化提供基础。

简介：崔炜皞，新加坡国立大学与上海交通大学联合培养博士后研究员，2023 年获上海交通大学计算机科学与工程博士学位。主要从事机器学习系统研究，聚焦大模型训练与推理基础设施、GPU 性能优化及智能体驱动的系统优化。已在 OSDI、ASPLOS、NSDI、HPCA、SC 等国际会议发表多篇论文，入选 2025 年度 CCF 博士学位论文激励计划。

2. 报告人：柳清源 技术专家

题目：AI 云基础设施的成本效益优化与工业实践

摘要：在 AI 时代，随着云计算的持续演进，云服务暴露给用户的抽象层次不断提升，运维复杂性也从用户侧逐渐向云服务提供商一侧转移。AI 云基础设施需要承担编排调度、资源规划等职责，并且需要面向具体场景满足相应的服务质量要求。在高度动态的云场景下，云基础设施如何在履行这些职责的同时，提升云任务运行的成本效益，是云服务提供商最关注的问题之一。本次报告主要讲述如何通过一系列创新成果，对大模型推理等典型云计算范式的多个维度的成本效益进行优化提升。同时，报告结合阿里云百炼的技术创新，介绍生产级云（推理）基础设施效率优化的工业实践。

简介：柳清源，阿里巴巴百炼云平台技术专家，博士期间聚焦云计算基础设施系统软件的全栈效能优化，旨在为通用计算任务与大模型推理任务提供高性能、低成本且易开发的底层支撑，在ATC, FAST, ISCA等操作系统、体系结构与云计算领域的顶会顶刊发表一作论文共 7 篇。其中，一系列工作已产生学术和工业影响力，包括：由其作为主要作者构建的相关基准ServerlessBench已获351次引用，为该领域最受关注的基准项目之一；其综合分析工业界与学术界 Serverless 研究的相关成果，成为SoCC首篇来自中国大陆的Vision Track论文；CHIME [ISCA'26] 的早期版本一周内获alphaXiv 358次点赞并进入趋势榜前五；SysSpec [FAST'26, TOS] 同获USENIX FAST Erik Riedel最佳论文奖和杰出技术成果奖，成为FAST自创办以来首个同获两奖的工作。

3. 报告人：李佳 清华大学人工智能学院 助理教授/特聘研究员

题目：迈向可信Coding Agent：挑战与实践

摘要：基于大模型的Coding Agent正在显著提升软件开发效率，推动开发方式从辅助编码向自主完成复杂任务演进。然而，随着开发效率成倍提升，面对海量AI生成的代码，一个关键问题日益凸显：Coding Agent值得信任吗？本次报告将从执行过程与交付结果两个层面，剖析当前Coding Agent面临的可信性挑战，例如：执行过程中被恶意劫持、生成包含安全漏洞的代码、故意欺骗用户等等；并进一步讨论如何提升Coding Agent可信性的方法。

简介：李佳，清华大学人工智能学院助理教授、特聘研究员，中国计算机学会（CCF）软件工程专业委员会委员。2025年获北京大学博士学位，师从金芝教授和李戈教授。主要从事人工智能与软件工程交叉研究，包括代码大模型与代码智能体。近五年在NeurIPS、ACL、ICSE、ASE等CCF A类会议及期刊发表论文30余篇，其中多篇入选口头报告（Oral）和Featured Article，论文累计被引用3100余次。相关研究（如aiXcoder-7B、DevEval、EvoCodeBench、结构化思维链）受到麻省理工学院、斯坦福大学等机构研究者的关注与讨论，并获中国科技网、《中国日报》等媒体报道。主持国家自然科学基金青年科学基金项目（C类）、北京市自然科学基金等科研项目，部分研究成果已实现应用转化，服务全球数百万开发者。曾获CCF软件工程专委优秀博士学位论文奖等荣誉。

4. 报告人：孙茂林 南京大学计算机学院博士研究生

题目：约束求解器测试的探索与实践

摘要：约束求解器是程序分析、软件验证与自动推理的重要基础设施，其正确性直接影响上层应用的可靠性。然而，求解器支持的逻辑理论多样、内部优化复杂，如何生成能够触发深层缺陷的测试输入，以及如何有效判定求解结果的正确性，仍是求解器测试面临的关键挑战。本报告将介绍我们在约束求解器测试方面的系列研究，重点讨论大语言模型辅助的测试输入生成、基于等价饱和的重写规则测试，以及面向优化求解器的跨理论近似验证。结合真实求解器中的缺陷案例，分享不同测试方法的设计思路与实践经验，并讨论相关方法向其他基础软件测试场景拓展的研究机会。

简介：孙茂林，南京大学计算机学院博士研究生，师从杨已彪研究员和周毓明教授，隶属徐宝文教授团队。主要研究方向为软件分析与测试，重点关注约束求解器与编译工具链的缺陷检测，以及大语言模型辅助的软件质量保障。已在ASPLOS、OOPSLA、ICSE、FSE、ISSTA、TOSEM、TSE等CCF-A类会议和期刊发表论文20余篇，其中以第一作者身份发表8篇，并曾获ACM SIGSOFT Distinguished Paper Award（ISSTA 2026）。在GCC、LLVM、Z3等开源基础软件中累计报告缺陷600余个。主持国家自然科学基金青年学生基础研究项目，入选中国科协青年科技人才培育工程博士生专项计划。

5. 报告人：李博涵 助理研究员

题目：SMT的局部搜索技术与应用

摘要：可满足模理论 (SMT) 已广泛应用于软件分析、验证和测试。本次报告聚焦于算术理论上的 SMT 问题，目前该领域的主流求解范式是 DPLL(T) 框架。然而，DPLL(T) 高度依赖 SAT 求解器与理论求解器之间的交互，在处理复杂理论时往往会出现显著的性能退化。尽管局部搜索 (Local Search) 作为一种不完备算法在 SAT 领域取得了巨大成功，但由于固有的技术挑战，将其扩展到算术理论 SMT 领域仍有待深入探索。因此，如何将局部搜索技术有效地集成到算术理论 SMT 中，并实现与主流方法相媲美的性能，具有极高的研究价值。本报告将深入探讨SMT的局部搜索算法及其实际应用。

简介：李博涵，中国科学院工业人工智能研究所助理研究员。于2025年在中国科学院软件研究所获得博士学位。其研究方向主要集中在满足模理论 (SMT) 的求解算法及其应用，已在 CAV、FM、ICSE、ToCL、CP等国际顶级学术会议及期刊上发表论文十余篇，并多次在国际SMT竞赛中斩获冠军，其中包括国内首次在该赛事夺冠。主持国家自然科学基金(C类)、CCF-华为胡杨林基金、江苏省重点实验室面上等多项科研项目。其曾荣获中国科学院院长奖，并入选CCF形式化方法专委会"博士学位论文激励计划"。

6. 报告人：赵韩蕊 博士后

题目：AI赋能的安全证书综合与形式化验证方法

摘要：随着人工智能技术逐步应用于自动驾驶、机器人等安全攸关领域，如何为具有复杂非线性动力学和神经网络控制策略的智能系统提供严格、可证明的安全保障，已成为可信人工智能与形式化方法交叉领域的重要研究问题。安全证书通过将系统性质转化为一组可验证的数学条件，为无限时间范围内的形式化验证提供了重要途径。然而，传统证书综合方法高度依赖预设模板与数值优化，在复杂、高维和强非线性系统中存在一定局限性。本报告围绕人工智能与形式化方法的深度融合，探索人工智能在表示、学习与搜索方面的能力，提升安全证书综合及复杂系统验证的自动化程度与可扩展性，同时借助形式化方法为智能系统的学习、决策与控制提供可证明的安全保障。在此基础上，进一步探讨面向感知不确定性和复杂开放环境的可信智能系统验证问题，并展望AI与形式化方法双向赋能的发展方向。

简介：赵韩蕊，国防科技大学计算机学院博士后，CCF形式化方法专委会通讯委员，主要从事形式化验证与可信人工智能研究，研究方向包括神经网络控制系统安全验证、安全证书综合与安全强化学习等。相关成果发表于FM、EMSOFT、DAC、CVPR、ICML、IEEE TCAD、ACM TECS等形式化方法与人工智能领域重要国际会议和期刊，曾获EMSOFT 2024最佳论文提名。正在主持中国博士后科学基金面上资助项目、国家自然科学基金青年科学基金项目、湖南省自然科学基金青年科学基金项目，并参与国家自然科学基金重大研究计划等。2025年博士毕业于华东师范大学，博士学位论文获2025年CCF形式化方法专委会博士学位论文激励计划提名。曾受邀在2023年CCF优秀博士生论坛、2024年CCF软件工程女性学者论坛等作学术报告。

五、论坛组织委员会简介

1. 论坛组委会：李明煜 副研究员

简介：李明煜，中国科学院软件研究所副研究员。从事操作系统、机密计算系统研究，相关成果发表于OSDI、EuroSys等计算机系统领域国际旗舰会议。团队研发大模型友好的操作系统新接口；加速国产鲲鹏服务器高斯密态数据库，代码贡献到openEuler、openGauss等国产开源项目主线。担任CCF系统软件专委会执委、AgenticOS程序委员会委员、开源鸿蒙具身智能操作系统项目管理委员会委员。

2. 论坛组委会：印莹 副教授

简介：印莹，东北大学计算机科学与工程学院副教授、博士生导师，CCF 软件工程专委会委员。研究方向为智能软件工程、数据库、推荐系统。在 CCF A 类会议 ESEC/FSE等高水平期刊会议发表论文100余篇。提出结构-序列转换驱动的细粒度代码缺陷识别方法，面向编程教学场景，研发了可实现代码缺陷定位、可解释诊断与修复推荐的人工智能赋能的交互式一体化编程自学平台-斑码（BanMa）。主持国家自然科学基金等国家及省部级课题10项；参与 863、973子课题、国家自然科学基金等项目10余项；授权发明专利20项。指导学生在 ACM-ICPC 国际大学生程序设计竞赛、全国大学生数学建模竞赛中获奖，并斩获 CCF BigData 最佳学生论文奖等多项学术与学科竞赛荣誉。

3. 论坛组委会：张昕荻 助理研究员

简介：张昕荻，中国科学院软件研究所，特别研究助理，主要研究SAT求解及形式化验证。他曾获得国际SAT协会"最佳博士学位论文奖"（亚洲首项）、国际SAT会议"最佳论文奖"（亚洲首项），研制的求解器于国际SAT、SMT、FLoC竞赛多次获冠军。SAT求解技术落地于国内多家EDA企业，并助力突破多个密码分析问题边界。主持或参与国自然青年基金、重点研发、中科院战略先导A等项目；于DAC、SAT、FM等领域顶会/期刊发表论文二十余篇。