本论坛聚焦研究热点和最新研究进展，邀请优秀学者到 ccf 中国软件大会介绍其工作并传授科研经验，以期带动软件领域的相关研究人员做出更高水平的学术贡献，发表高层次的学术论文。本论坛邀请了来自于中科院软件所的蔡少伟、清华大学的姜宇以及上海交通大学的陈榕等三位学术界的前沿研究者做特邀报告，讲授形式化方法、软件工程、系统软件领域前沿技术以及从事高水平前沿科学研究的经验。本论坛邀请了今年ccf a 类论文的作者作为论坛演讲嘉宾，在介绍研究工作的同时，也介绍在科研选题、破题、实验、写作以及推广应用等方面的经验和教训。本论坛一共有10篇论文获得 ccf a 类会议的最佳论文或者杰出论文奖。

01

论坛组织委员会

陈振邦（国防科技大学）

夏虞斌（上海交通大学）

姜艳杰（北京大学）

02

论坛议程

03

论坛报告嘉宾简介

蔡少伟

报告题目：约束求解器的两端：大算力与小算力

报告摘要：

约束求解器，尤其是sat和smt求解，是硬件和软件的可靠性保障的基础引擎。约束求解的研究长期聚焦于普通算力下的算法，该方向的发展在多年之后也遇到了瓶颈，然而仍然无法很好解决工业需求。很多工业需求如软件验证涉及超出已有求解器可求解规模/难度的任务，也有些工业需求如终端实时任务要求小内存且快速响应。这都需要我们跳出普通算力的框架来研究约束求解。本报告介绍我们在分布式求解器的进展，相应smt求解器可以求解许多串行算法解决不了的实例。报告也介绍smt求解器应用于终端页面自动适配任务达到10ms以内实时响应。相关工作对应于cav 2024杰出论文奖和华为鸿蒙创新大赛top 10的成果。

报告人简介：

蔡少伟，中科院软件所研究员，博导，研究约束求解和形式化验证，获得相关领域顶级会议cav，sat，cp等会议的最佳/杰出论文奖，多次获得sat比赛，smt比赛和maxsat比赛的冠军，带领团队研发了eda形式化验证工具。研发的求解器应用于eda和操作系统验证，包括多个eda公司以及应用于华为鸿蒙操作系统。

姜宇

报告题目：面向复杂系统软件的模糊测试研究与实践

报告摘要：

模糊测试是一种有效的缺陷检测技术，但是在面对复杂系统软件时，如操作系统和数据库系统，依然存在三个突出难点：（1）无法有效监测覆盖信息。系统软件往往有着高度复杂的逻辑，而粗略记录的特征在大规模代码中存在冲突和不精确的情况。（2）无法高效生成有效输入。系统软件具有复杂的输入规范，而现有机制会生成大量系统软件无法接受的无用输入。（3）无法监测程序异常。系统软件具有守护进程等机制，会在执行过程中对遇到的异常进行处理或异常恢复，而使模糊测试工具无法捕获程序异常。本报告将围绕模糊测试的现状和上述针对系统软件的难点展开，并介绍操作系统与数据库系统这两类典型系统软件的模糊测试关键技术与实践。

报告人简介：

姜宇，清华大学软件学院副教授，科技部重点研发计划项目负责人，统信-羽林操作系统供应链安全实验室主任。重点关注操作系统、数据库、浏览器、协议等基础软件的测试与防护，在mysql、safari和linux等广泛使用的系统软件中挖掘300 漏洞被收入中美国家信息安全漏洞库。研发的自动化模糊测试技术被并入谷歌clusterfuzz，微软onefuzz等平台。在sosp、sigmod、s&p和pldi等会议和期刊上发表论文100余篇，获fse和security等会议的杰出论文或提名奖6次。主持基金委优秀青年科学基金、华为大颗粒研究计划等项目30余项。曾获2015年ccf优秀博士论文奖、2020年阿里巴巴达摩院青橙奖、2022年nasac青年软件创新奖、2024年ccf技术发明一等奖等奖励。

陈榕

报告题目：面向智能应用的大算力硬件调度与管理

报告摘要：

人工智能时代硬件能力与应用需求都迎来了重大突破与革新，为基础系统软件究带来了机遇与挑战。本次报告将分享我们对于基础系统软件在人工智能时代承担角色和研究方向的初步思考，并介绍我们近期面向智能应用的突出需求，从以gpu为代表的大算力硬件的调度和管理入手，对于共性难题和前沿技术开展的研究工作以及收获。

报告人简介：

陈榕，上海交通大学教授、ccf杰出会员。主要研究领域为操作系统、分布式系统等基础系统软件。在计算机系统领域ccf a类会议/期刊发表论文30余篇，包括了13篇osdi/sosp、12篇eurosys/atc，并多次获得eurosys等ccf a类国际会议最佳论文奖。受邀担任osdi、sosp等本领域重要会议程序委员会委员。曾荣获国家技术发明二等奖、上海市和教育部技术发明一等奖、以及华为奥林帕斯先锋奖等。

王迪

报告题目：保证引导程序组合正确性的可编程mcmc

报告摘要：

概率编程语言（ppl）为灵活表达概率模型和进行贝叶斯推理提供了语言支持。具有可编程推理功能的ppl允许用户通过定制与模型程序匹配的引导程序来改进推理。然而，引导程序中的错误可能会破坏推理的正确性。报告将介绍一个基于协程的框架来保证一类mcmc推理算法中用户编写的引导程序的正确性。该框架基于一种新型类型系统，该系统描述了模型程序与一系列仅更新部分随机变量的引导程序之间的通信协议，并且支持多项式时间的类型等价性判定，进而支持高效的类型推断算法。该框架还包括一个覆盖检查算法，它能够验证多个引导程序组合在一起时是否和模型程序适配。实验表明，该框架的类型推断和覆盖检查可以高效地检查现有静态分析无法处理的正确或错误的引导程序。

报告人简介：

王迪是北京大学计算机学院的助理教授。他于2022年在美国卡内基梅隆大学获得博士学位，于2017年在北京大学获得学士学位。他的研究兴趣包括形式化验证、程序分析、类型系统以及概率编程，目前的研究项目涉及资源安全的系统编程、可编程贝叶斯推断、量化程序分析以及面向证明的编程语言。他获得了国家优秀青年科学基金项目（海外）资助，多项研究成果发表于编程语言领域的顶级会议popl、pldi、oopsla、icfp等。

孙璞

报告题目：easybc：一种面向分组密码差分分析全自动安全性评估的特定领域语言

报告摘要：

差分密码分析是一种强大的算法级攻击方法，在评估对称密码原语的安全性方面起着核心作用。一般而言，对差分密码分析的抵抗能力可以通过最大期望差分特征概率来表征。本报告介绍一种基于混合整数线性规划（milp）的通用和可扩展方法，以界定此类概率。通过设计一种针对分组密码的高级密码特定语言easybc，并提供了各种严格的程序作为差分表示语义，以自动化从用easybc编写的分组密码生成 milp 的过程。通过实现的一个开源工具，对包括所有10个 nist 轻量级密码标准化过程的决赛候选密码在内的23种现实生活中的密码原语上进行了广泛评估。easybc使得对差分密码分析的抵抗评估变得更加易于访问，为密码学研究者提供了便利。

报告人简介：

孙璞，铜陵学院数学与计算机学院讲师，获上海科技大学计算机科学与技术专业博士学位。主要研究方向为密码分析、形式化验证。在国内外期刊会议发表文章4篇。

时清凯

报告题目：基于静态程序分析的网络协议逆向工程与漏洞检测

报告摘要：

网络协议定义计算机系统如何相互连接，因此，网络协议漏洞可能造成灾难性严重后果。网络协议的形式化规格说明是各种自动化网络安全分析（如模糊测试、网络监听、模型检测等）的基础，因此格外重要。该报告将介绍报告人关于网络协议逆向工程的相关工作，其主要思路为通过静态程序分析的手段，分析网络协议的实现，构建包含精确语法结构和语义的网络协议规格说明，并使用构建的精确规格说明指导下游网络安全分析。截止目前，该工作已找到50余个网络协议中的严重漏洞，包括缓冲区溢出、整数溢出等，并获得10余个cve编号。

报告人简介：

时清凯，南京大学计算机学院副教授，博士生导师，紫金学者，国家级高层次青年人才，2020年于香港科技大学获得博士学位，曾任源伞科技联合创始人、蚂蚁集团技术专家、美国普渡大学博士后研究员。目前主要从事编译技术及基于编译的软件安全技术研究，其研究成果广泛发表于程序语言、网络安全、软件工程等ccf a类会议或期刊，曾获acm sigsoft杰出论文奖一次、acm sigplan杰出论文奖两次、谷歌论文奖一次等，曾三次参加中国软件大会软件原型竞赛，均获一等奖。

姚培森

报告题目：一种路径敏感数据依赖分析方法

报告摘要：

本文提出了一种可扩展的路径敏感、上下文敏感数据依赖分析方法。通过将析取推理分解为1)半路径敏感预分析, 2)全路径敏感按需分析，该方法缓解了构建精确内存模型时的“别名路径爆炸”问题。我们将该方法应用于不同分析场景（程序切片和漏洞挖掘），并与多种先进分析技术进行比较，展示了其在精度和可扩展性上的显著优势.

报告人简介：

浙江大学“百人计划“研究员、博士生导师，ccf 形式化方法专委、理论计算机科学专委执行委员，acm sigplan、sigsac会员，入选国家青年人才计划。主要研究方向为编程语言(程序分析与验证、程序合成与优化)，数理逻辑(自动定理证明)，软件安全（漏洞挖掘）。相关成果发表于编程语言(pldi, oopsla)、软件工程(icse, esec/fse, issta, ase, tosem)、信息安全(s&p, usenix security, tdsc)、计算机系统(asplos)等领域的ccf-a会议或期刊，获acm sigplan杰出论文奖、 acm sigsoft杰出论文奖、google research paper rewards等奖项, 发现linux kernel、mysql、firefox等开源程序数百个真实缺陷。担任相关领域顶级会议(popl 2025, oopsla 2025, pldi 2023, ccs 2024, issta 20224)程序委员会委员。详情见 https://rainoftime.github.io/

王栋

报告题目：基于大语言模型的等价变异检测

报告摘要：

变异测试对于确保软件质量至关重要。然而，等价变异体的存在会引入冗余成本和偏差问题，阻碍变异测试在实际应用中的有效性。尽管许多等价变异检测 (emd) 技术被提出，但由于训练数据稀缺以及难以推广到未见过的变异体，这些技术仍存在显著局限。最近，大语言模型 (llm) 已广泛应用于各类代码相关任务，并凭借其对程序语义的精准捕捉展现出卓越的性能。但是，llm在等价变异检测中的表现尚不清楚。因此，我们对数千个java变异代码进行了实证研究，以全面研究llm在等价变异检测上的有效性和效率。具体而言，我们评估了llm与现有emd技术的性能，分析了llm的各种应用策略，考察了emd技术间的正交性，并测量了训练和推理的时间开销。结果表明，基于llm的技术明显优于现有emd技术，其中微调代码嵌入策略最为有效。此外，基于llm的技术在时间成本和有效性之间实现了极好的平衡。根据研究结果，我们进一步讨论了模型规模和代码嵌入质量的影响，并为未来研究指明了方向。这项工作首次在等价变异检测中评估了llm，验证了其有效性和效率。

报告人简介：

王栋，天津大学副研究员，研究方向包括软件仓库挖掘、智能化软件工程及软件安全。研究目标是从软件仓库的历史数据中提取知识，揭示实证证据，获取对软件工程管理有用的洞察，并开发支持开发人员的自动化方法。近5年来他在国际会议和期刊共发表 20 余篇论文，涵盖 icse、issta、ase、tse、tosem、emse 等顶级软工会议与期刊，获得issta24杰出论文奖。此外，在软件工程领域的旗舰会议和期刊中广泛担任审稿人和组织者，包括 icse,ase,tse,tosem,emse。

王尚文

报告题目：左右开弓—人类实践制导的多粒度补丁生成技术

报告摘要：

自动修复软件代码中的缺陷一直是工业界与学术界共同的梦想，近年来，基于深度学习的方法正为这一梦想的实现注入强大的动力。然而，基于深度学习的软件自动修复技术或是聚焦于代码token的补全、或是致力于代码语句的翻译，往往仅从单一的粒度出发，尝试生成补丁。本文通过大规模实证分析发现，在修复缺陷的实践活动中，开发人员往往会在多个粒度上编写补丁，包括语句级、表达式级以及token级，且各个粒度的比例大致相当。受此启发，本文提出借鉴左右开弓的思想来实现软件修复，在上述三种粒度上均尝试生成补丁，并依靠一个简单的启发式筛选出正确补丁。实验结果表明所提方法兼具实用性与通用性：相较已有方法，该方法在defects4j缺陷数据集上正确修复了更多缺陷，并且具备更强的软件漏洞修复能力。

报告人简介：

王尚文，国防科技大学助理研究员、2023届优秀毕业生，主要从事缺陷定位与程序修复、智能化软件工程方面的研究，在oopsla、icse、fse、ase、issta、tse、tosem等顶级会议和期刊上发表论文20余篇，主持国家自然科学基金青年基金、国防科技大学青年自主创新科学基金在内的多项科研项目。担任tse、tosem、emse等国际期刊的审稿人以及ccs、icse、ase等国际会议的程序委员会委员。获acm sigsoft杰出论文奖1次，ieee tcse杰出论文奖2次。

孙海龙

报告题目：深度神经网络模型的模块化分解与按需复用

报告摘要：

提高深度神经网络模型的构建效率和质量是人工智能领域的重要问题。受经典软件复用方法的启发，我们提出了以“分而治之，集成汇聚”为主要特征的群智化模型构建与优化方法，其核心是基于模块分解和按需组合的模型复用。报告聚焦深度神经网络模型的复用问题，分析模型复用的研究动机和挑战，介绍深度神经网络模型模块化技术的研究进展，重点介绍近期提出的“训练时”模块化技术，最后给出关于未来工作的思考。

报告人简介：

孙海龙，ccf杰出会员、ccf协同计算专委副主任、ccf开源发展委员会执行委员。北京航空航天大学教授。主要研究群体智能、智能软件工程和开源软件等方向。主持了国家重点研发计划项目、国家自然科学基金专项重点支持项目等。在tosem、icse、aaai、kdd和osdi等发表论文100余篇，获国际会议最佳/杰出论文奖4项，1篇论文被推荐为kdd’23最佳论文候选，曾获2项国家技术发明二等奖。

胡星

报告题目：代码检索：大模型下代码生成的最后一公里

报告摘要：

近年来，大模型展现出了强大的智能涌现能力，在自然语言处理等任务中表现出了出色的自主学习和推理能力。在软件工程领域，使用大模型提升软件开发效率，保障软件质量成为当前研究热点，例如copilot集成了最新的大模型并用于代码生成。然而，大模型的应用面临诸多挑战。例如，在特定编程语言、特定场景下，其代码生成能力不佳。因此，本次报告将探讨如何更好的利用代码检索技术进一步增强大模型代码生成的能力。

报告人简介：

胡星， 浙江大学软件学院副教授，主要研究方向为智能化软件工程，程序理解，软件仓库挖掘。在tosem、icse、ase、fse和emse等高水平会议和期刊上发表论文40余篇。担任tosem，jsep期刊编委。主持国家自然科学基金专项培育项目，参与国家重点研发计划等多个科研项目。获得icse2024 acm sigsoft distinguished paper award，msr 2024 acm sigsoft distinguished paper award，icpc 2018 acm sigsoft distinguished paper award。担任forge2024和internetware2023程序委员会主席，担任国际级顶级期刊（tse、tosem、emse）审稿人，受邀担任国际会议ase、icse、fse、issta、msr、icsme、saner的程序委员会成员。详情请参考个人凯发k8登录主页：https://xing-hu.github.io/

徐梦炜

报告题目：rust os和卫星

报告摘要：

卫星星座已经成为地面算网基础设施的重要拓展，被认为是下一代核心计算平台。由于卫星任务和空间环境的复杂性，构建高可靠、高效率的卫星系统软件对未来卫星通讯和计算的发展至关重要。本次报告会重点分享团队在构建开源rust操作系统rros（https://github.com/bupt-os/rros）过程中的挑战和经验，以及对其重要依赖模块rust-for-linux的实证分析结果。

报告人简介：

徐梦炜，北京邮电大学计算机学院副教授，博士生导师。于北京大学获得本科与博士学位，入选中国科协青年人才托举工程，北京市科技新星，微软亚洲研究院“铸星计划”访问学者，普渡大学访问学者。主要研究领域为移动/边缘计算和系统软件，相关成果发表于acm mobicom/mobisys/asplos /ieee tmc/软件学报等国内外顶级会议期刊，获usenix atc 2024最佳论文奖。主持国家自然科学基金、科技部重点研发项目课题等多个项目。

魏星达

报告题目：面向服务器无感知计算的高效通信原语

报告摘要：

服务器无感计算是一种新兴的云计算范式，能够按需启动所需的计算容器，显著提高云平台的资源利用率和计算性价比。然而，容器间的隔离增加了跨容器通信的开销，从而显著影响应用性能。为此，我们提出了一种新型操作系统原语——remote map。该原语可以动态融合不同（跨节点）容器间的虚拟内存边界，从而大幅提升服务器无感计算环境中的应用通信性能。

报告人简介：

魏星达，上海交通大学助理教授。主要研究方向为分布式系统和操作系统，最近主要的关注点为如何在ai和serverless下，提升计算和存储基础系统软件的性能、可靠性和运行成本。在包括osdi/sosp、eurosys、nsdi等会议上发表多篇论文。曾获eurosys2024最佳论文，2022年华为火花奖，2021年acm sigops dennis m. ritchie award优胜奖，2020年华为奥林帕斯先锋奖等多个奖项。博士论文获2021年acm 中国优秀博士学位论文提名奖，acm chinasys优秀博士论文奖。担任包括osdi，asplos和nsdi在内的多个期刊审稿人及国际会议程序委员会成员。

徐尔茨

报告题目：从“小软件”到“大系统“---工业界视角下的系统软件科研

报告摘要：

当前系统软件研究的一个发展趋势就是学术界和工业界的紧密结合。一方面，工业界系统能够提供丰富的数据、实际的问题和大规模的验证环境等有利条件。同时，由于关注点、视野和一些潜在不可控因素，学术界的老师与学生在合作过程中，往往并非一帆风顺，甚至有可能”中道崩殂“。本次报告，通过报告人从前期较为成功的合作案例出发，从小型优化（perseus@fast’23)和大系统研发（ebs@fast’24）两个角度探讨工业界视角下的系统软件科研的一些经验和教训。

报告人简介：

徐尔茨博士，长期从事分布式存储系统和软硬件可靠性研究。他的研究成果在多个顶级会议上，包括usenix osdi、fast、atc和acm eurosys等共计二十余篇ccf国际a类会议，在cs ranking统计的近五年系统类顶会论文发表中位居全球前二十。他是两届usenix fast最佳论文奖（fast'23, fast'24）和2023 acm sigops中国新星奖的获得者。徐博士还担任了fast、nsdi、atc、eurosys等多个国际学术会议程序委员会委员。

刘宏远

报告题目：ngap: 基于gpu的非阻塞大规模自动机处理

报告摘要：

有限自动机作为计算核心被广泛应用于各种需要高吞吐量的场景中。然而，尽管gpu的计算能力不断增强，其在处理自动机方面的潜力却未能得到充分利用。在这项工作中，我们识别出限制gpu吞吐量的三大主要挑战：1) 可用的并行性不足，导致gpu线程未被充分利用；2) 自动机工作负载涉及大量冗余计算，因为部分状态会匹配重复的符号；3) 线程与状态之间的映射会动态切换，导致数据局部性较差。我们的关键见解是，按“每次处理一个符号”的方式执行自动机处理会使执行过程串行化，因此需要进行改进。为了解决这些挑战，我们提出了非阻塞自动机处理方法，该方法允许输入流中的不同符号并行处理，并实现了进一步的优化：1) 我们预取一部分计算内容，以提高同时处理多个符号的机会，从而更好地利用gpu线程；2) 为了减少冗余计算，我们将重复的计算结果存储在一个记忆化表中，借助表查找替代这些重复计算；3) 我们对部分计算进行私有化，以保持线程与状态之间的映射，从而改善数据局部性。实验结果表明，我们的方法在20个应用场景中平均性能超过最先进的gpu自动机处理引擎7.9倍，最高提升可达901倍。

报告人简介：

刘宏远是香港科技大学（广州）的一名助理教授，专注于计算机体系结构和高性能计算。他的研究主要致力于优化gpu上不规则应用的性能，旨在提升在不规则控制流、内存访问模式和并行性等场景下的计算效率。他在威廉与玛丽学院获得博士学位。2019年秋季，他在英特尔实习，2021年春季曾作为访问学生在阿贡国家实验室学习。在从事学术生涯之前，他曾在百度担任软件工程师。他拥有山东大学的学士学位和香港大学的硕士学位。他的研究在asplos 2024会议上获得了最佳论文奖。

04

论坛组织委员会简介

论坛主席：陈振邦

个人简介：

国防科技大学计算机学院教授、博士生导师，主要研究方向为程序分析、形式化方法及其在不同背景下的应用。近年来主要围绕符号执行相关的理论、技术和应用开展研究，成果发表在 icse、fse、issta、ase、fm、tcs 等重要国际会议或期刊上，获 acm sigsoft 杰出论文奖 2 次。获国家科技进步二等奖 1 项、省部级科技进步二等奖 2 项，获 nasac 青年软件创新奖。

论坛主席：夏虞斌

个人简介：

夏虞斌，上海交通大学教授，上海市优秀学术带头人，ccf杰出会员，国家级青年人才计划入选者，“挑战杯”全国特等奖优秀指导老师。担任osdi、eurosys等操作系统国际会议的评审委员会委员。openharmony技术支撑组成员，上海交通大学openharmony技术俱乐部主任。

论坛主席：姜艳杰

个人简介：

北京大学全职博士后，师从张路教授、刘辉教授。研究方向包括软件代码的自然语言处理和软件缺陷。在 fse、icse、tse、tosem、ase、issta 等 ccf a 类会议 / 期刊上发表论文十余篇，获esec/fse 2023杰出论文奖。作为项目负责人承担博士后创新人才支持计划、博士后面上项目和ccf-华为胡杨林基金。