CCF ChinaSoft 2023 论坛巡礼 | 顶会顶刊论坛

2023年CCF中国软件大会（CCF ChinaSoft 2023）由CCF主办，CCF系统软件专委会、形式化方法专委会、软件工程专委会以及复旦大学联合承办，将于2023年12月1-3日在上海国际会议中心举行。

本次大会主题是“智能化软件创新推动数字经济与社会发展”，学术、工业、教育、竞赛等分论坛活动40余场，期待您的参与！

目前大会火热报名中！

CCF ChinaSoft 2023官方首页：

http://chinasoft.ccf.org.cn/

点击文末“阅读原文”进入官方注册通道:

https://conf.ccf.org.cn/chinasoft2023

✦ +

论坛巡礼

论坛名称：顶会顶刊论坛

时间: 2023年12月1日（星期五），08:30 – 18:00

地点: 上海国际会议中心，3楼黄河厅

论坛简介：

本论坛聚焦研究热点和最新研究进展，邀请优秀学者到 CCF 中国软件大会介绍其工作并传授科研经验，以期带动软件领域的相关研究人员做出更高水平的学术贡献，发表高层次的学术论文。

本论坛邀请了来自于华中科技大学的华宇、清华大学的贺飞、华为公司的夏鑫等三位学术界、工业界的前沿研究者做特邀报告，讲授软件工程、系统软件、形式化方法领域前沿技术以及从事高水平前沿科学研究的经验。本论坛邀请了今年发表于 CCF A 类会议/期刊的论文作者作为论坛演讲嘉宾，介绍他们在科研选题、破题、实验、写作以及推广应用等方面的经验和教训。其中6篇论文获得CCF A类会议的最佳论文或者杰出论文奖。

日程安排

Schedule

论坛主席

Forum Chairmen

陈雨亭

上海交通大学

副教授，博士生导师，主要研究可信的软件运行环境、程序分析与测试技术，在 TOSEM、 TSE、 PLDI、 ICSE、 FSE、ISSTA、 ASE 重要国际会议与期刊上发表或被接收过约 80 篇论文；曾主持、参与国家自然科学基金项目、科技部重点研发项目 10余项。获 NASAC-东软青年软件创新奖、 ICSE 2023 杰出论文奖等。

陈振邦

国防科技大学

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

姜艳杰

北京大学

北京大学全职博士后，师从张路教授、刘辉教授。研究方向包括软件代码的自然语言处理：关注代码的文本语义，重点解决代码中缩写词的扩展与解读问题；软件缺陷：研究大规模高质量软件缺陷库的自动化构建方法，构建了缺陷库GrowingBugs。在ESEC/FSE、ICSE、TSE、ASE、ISSTA等CCF A类会议/期刊上发表论文十余篇。

论坛嘉宾

Forum Guests

贺飞

清华大学

清华大学长聘副教授，博士生导师。主要从事程序验证、模型检验和自动推理的研究。开发了模型检验和程序验证工具，并在中航、中车、华为等公司进行应用。在形式化方法、程序语言和软件工程的重要国际会议和期刊上发表论文80余篇。入选国家某青年人才计划和“中创软件人才奖”，曾获并行编程旗舰会议PPoPP 2022最佳论文奖、软件工程顶会ASE 2018杰出论文奖、形式化方法会议SETTA 2022最佳论文奖等。

报告题目：

程序终止性分析的若干进展

报告摘要：

程序终止性问题是程序验证领域的一个经典难题，关注程序是否在所有输入情况下都能结束执行。该问题属于不可判定问题，即不存在一种通用算法能够确定所有程序的终止性。本报告将介绍我们在程序终止性和非终止性证明领域取得的一些最新研究成果，并对概率程序和演化程序的终止性分析进行讨论。

夏鑫

华为软件工程应用技术实验室主任

夏鑫目前担任华为软件工程应用技术实验室主任。他的研究方向是智能化软件工程、软件仓库挖掘和经验软件工程。夏鑫至今发表了300多篇论文，其中包括130多篇CCF A类期刊和会议长文，谷歌学术引用1.3万多次，H-index 64。夏鑫获得了2022年ACM SIGSOFT Early Career Researcher Award（亚太地区第一位），部分论文获得国际会议最佳/杰出论文奖项，包括6篇ACM SIGSOFT 杰出论文奖（连续四年获得软工顶会ASE 2018-2021的杰出论文奖）。此外他担任MSR、SANER、PROMISE等会议的Steering Committee，多个国际会议的PC (ICSE，ESEC/FSE, ASE等)，多个期刊的编委（TOSEM、EMSE、ASEJ、JSEP等），以及参与组织了多个国际会议（ICSE 2023和2024， ASE 2016、2020和2021等）。更多信息在https://xin-xia.github.io/

报告题目：

大模型下的软件工程时代真的到来了吗？

报告摘要：

大模型在软件工程领域的应用越来越广泛，也引发了越来越多的争议。一方面，大量研究表明大模型可以极大促进研发效能；另一方面，大量研究也表明大模型在软件工程应用存在较大局限性。为此，在大模型时代下，我们的软件工程研究应该如何推进？本次报告主要汇报本人最近在软件工程大模型的一些初步探索，从大模型各种争议开始，介绍我们如何突破当前技术困境，并初步展望未来之路。

华宇

华中科技大学

华中科技大学教授，国家杰出青年科学基金获得者，CCF杰出会员和杰出演讲者。主要研究新型存储器件、高性能存储系统和安全架构。在OSDI、 ASPLOS、 MICRO、 FAST、 HPCA 等会议上发表多篇学术论文。在ICDCS 2021、ACM APSys 2019等国际会议上担任程序主席/副主席，在OSDI、 SIGCOMM、 FAST、 NSDI、ASPLOS、SC、EuroSys 等国际会议上担任程序委员，是ACM Transactions on Storage期刊的编委。研究成果获得教育部自然科学一等奖、湖北省科技进步一等奖，以及FAST 2023、 IWQoS 2023 等国际会议的最佳论文奖。指导的博士生获得ACM中国优博全国奖和CCF优博提名奖等。

报告题目：

大内存系统的第一原理

报告摘要：

大内存系统具有大容量、高性能、非易失等特点，以新型持久内存、CXL互联内存、池化内存等形式构建的大内存系统的软件体系正面临持久域加密难、存算体融合难和多通道风险高等难题。为有效解决大内存系统在系统软件方面存在的技术挑战，需要全面深入分析和研究大内存系统的第一原理，报告将从构建大内存系统软硬件生态体系的角度出发，在软件体系、分布式事务、加密机理等方面进行全面分析，并对其发展历程、功能组件、关联关系和系统验证等方面进行阐述。

蒋炎岩

南京大学

南京大学计算机科学与技术系新体制副教授。研究兴趣包括软件系统分析测试和软件自动化，在操作系统和软件工程顶级会议发表论文十余篇、担任多个重要会议的程序委员会委员，获NASAC青年软件创新奖、CCF优秀博士论文奖、SOSP’23 Best Paper Award、ICSE’21 ACM Europe Council Best Paper Award等荣誉或奖励。蒋炎岩执教了广受欢迎的《操作系统》课程，互联网播放超300百万次，多次获评“毕业生心目中的好课程”。蒋炎岩十多年来一直服务于江苏省青少年信息学奥林匹克竞赛委员会的命题和技术工作，他也是APIO2022、APIO2023的Technical Committee成员。

报告题目：

Just-in-Time编译器测试的新途径

报告摘要：

本次报告将介绍我们在对即时(Just-in-Time)编译的编译器进行系统化测试的工具。即时编译器经历漫长的预热过程，带来难以充分测试的困难。我们创新性地提出了程序的“编译空间”，并通过程序编译的方式对编译空间实现系统性地探索，从而暴露即时编译器中的缺陷。在我们的实验中，为三个广泛使用的生产JVM，即HotSpot，OpenJ9和Android Runtime报告了85个缺陷（均为即时编译器中的缺陷），其中已经确认或被修复了53个。

黄箐

江西师范大学

江西师范大学副教授，Prompt Sapper联合创始人，江西智能软件工程实验室负责人，CCF软件工程专委会委员。主持或参与多项国家自然科学基金项目（面上、青年、地区），近两年以第一作者身份发表CCF A类论文8篇，如TOSEM、TSC、ICSE 2022、ASE 2022、ASE 2023等。研究方向为智能软件工程，专注于探索解决领域知识与LLM通用知识有机融合核心科学问题的新思路。研究原创的自然语言原生AI编排方法、范式、体系、理论、技术、平台及典型应用。重点解决基础模型应用效率、技术门槛、推理能力、可控性和可解释性，以及人机交互体验等关键技术挑战。研制支持自然语言编程的一站式AI编排平台Sapper。该成果在多个场合获得广泛传播，包括江西卫视、知名公众号“机器之心”、江西省第四届成果对接会、2023年AI+软件研发数字峰会，甚至引起知名创业孵化期YC公司的关注和积极反馈。

报告题目：

基于动态提示微调预训练语言模型的API知识提取

报告摘要：

API的正确使用对高质量软件的功能、性能和安全至关重要，而API知识是确保API被正确使用的关键。然而，当前方法难以处理API知识的多义性问题，导致知识提取准确度下降。鉴于大型语言模型蕴含丰富的API语义信息，本研究提出一种动态提示微调模型的方法，将有限数量的多义性API知识与模型的通用能力有机融合，以激发模型对多义性API知识的理解能力。实验证明，所提方法在API知识提取方面优于传统方法，尤其是在训练数据稀缺情况下，仍能实现较高的知识提取准确度。该方法有望成为使用模型微调来解决特定领域问题的有力示范。

马菲菲

中国科学院软件研究所

中国科学院软件研究所研究员，博士生导师，中国科学院大学岗位教授。研究方向为自动推理、约束求解，成果发表于IJCAR、ISSAC、CP、SAT、TCS、IJCAI、AAAI、JAIR、NeurIPS、 ICCV、ISSTA、ASE等计算机科学、人工智能和软件工程等领域的高水平会议或期刊上。获ISSTA 2023 ACM SIGSOFT Distinguished Paper Award，中国科学院青年创新促进会优秀会员，省部级一等奖一项，省部级二等奖一项。

报告题目：

基于位展开求解非线性整数约束

报告摘要：

非线性整数约束是SMT领域中一个重要的约束类型，常出现在规划、软件/硬件验证和分析、自动化测试等实际问题中。在SMT领域，一类经典的方法是通过位展开(Bit-Blasting)将约束转化为对应的布尔可满足性问题进行求解。本文就非线性整数约束的求解，提出了一种基于位展开方法(Bit-Blasting)的求解框架和一系列优化策略，显著提升了求解效率。针对搜索域难以确定的问题，论文提出了应对非线性乘法和特定约束的确定位长的启发式策略，以寻找到合适的搜索空间；针对连续加法中不同顺序导致冗余的问题，论文提出了一个最优顺序决策算法并证明了其最优性。我们从零开始构建并实现了相应的SMT求解器——BLAN。与Z3、CVC5等主流SMT求解器相比，BLAN在可满足实例求解的性能上有了显著提升。

贾周阳

国防科技大学

博士，国防科技大学计算机学院助理研究员。国防科技大学本、硕、博，曾赴美国肯塔基大学联合培养两年。主要从事系统软件和软件可靠性方向相关研究，在ICSE、FSE、ASE等CCF推荐的期刊和会议中发表论文20余篇，获包括ICSE23在内的杰出论文奖4次。申请和授权专利10余项。获CCF优秀博士激励计划提名、全军优秀博士论文奖、湖南省湖湘青年英才、国防科技大学高层次创新人才培养对象。

报告题目：

理解和检测运行时配置更新缺陷

报告摘要：

大型软件系统通过引入越来越多的配置选项以提供灵活性，并通过支持运行时配置动态更新以提供持久化服务。然而这种机制可能会影响系统的可靠性，导致软件崩溃或功能错误等意外结果。我们将由运行时配置更新引起的缺陷称为On-the-fly Configuration Bugs，简称OCBugs。我们首先对来自5个大型系统的75个真实OCBugs进行了调研，了解其现象、根因和触发条件。基于调研结论，设计了自动化测试框架PARACHUTE以检测OCBugs。PARACHUTE通过变异现有的测试用例引入动态配置更新，再基于差分测试检测OCBugs。其主要原理是：无论在启动阶段加载还是在运行时更新，一个配置选项的值对目标程序应该具有相同的影响。我们在7个真实世界的软件系统上评估了PARACHUTE，发现可以检测75%（42/56）的已知OCBugs，并检测出13个未知的缺陷，其中11个被开发人员确认或修复。

王豫

南京大学

南京大学毓秀博士后。研究工作主要侧重于软件测试和智能化软件工程。研究成果在PLDI、OOPSLA、TSE、ISSTA、JCST、软件学报等国内外高水平期刊会议上发表十余篇论文。研发的部分工具获NASAC原型竞赛二等奖，且已经在阿里，华为等一流软件企业应用。

报告题目：

对代码模型的离散对抗性攻击方法

报告摘要：

近年来，深度神经网络的安全性备受关注，其中对抗攻击是一个典型的安全问题。对抗攻击指的是对神经网络输入进行微小且难以察觉的修改，却能够导致网络的预测结果发生变化。尽管对抗攻击方法已经取得了显著进展，但是无法有效用于预测程序性质的代码模型。这是因为代码模型中的源码和模型输入之间存在离散的对应关系，现有的对抗样本方法难以有效处理这种相关的代码模型。因此，本报告介绍了一种专门针对代码模型的对抗攻击方法，称为离散对抗攻击。该攻击方法通过对原始输入进行保留语义的程序转换来提高攻击的成功率。同时，本报告还从防御的角度介绍了一种用于防御代码模型的离散对抗攻击的理论，并基于该理论提出了一种朴素的对抗训练方法。实验结果表明，无论是否采用防御机制来增强模型的安全性，离散攻击方法都比当前最先进的方法更加有效。此外，对抗性训练能够有效提升代码模型的安全性。

李建文

华东师范大学

华东师范大学研究员，博士生导师，入选上海市青年人才计划，获得上海市浦江人才荣誉称号，主持国家自然科学基金面上项目、青年项目、重点项目课题各一项。研究方向主要为形式化自动验证技术，可用于保障计算机软硬件系统的正确性和安全性，重点应用场景包括芯片、航天、轨道交通等安全攸关领域。

报告题目：

通过搜索i-good引理来增强安全模型检验的性能

报告摘要：

IC3/PDR及其变体是近年来在安全性模型检验领域突出的方法。与以往的模型检验算法如BMC（有界模型检验）和IMC（插值模型检验）相比，IC3/PDR因其完备性（相对于BMC）和可扩展性（相对于IMC）而具有吸引力。IC3/PDR维护一个向上近似的状态序列以证明正确性。尽管序列精化方法被认为对性能至关重要，但文献中缺乏对这个问题的系统分析。我们提出了一种基于i-good引理定义的方法，引入了两种启发式方法，即branching和refer-skipping，以引导搜索朝着构建i-good引理的方向进行。这种方法适用于IC3及其变体CAR（互补逼近可达性），并且非常容易集成到现有系统中。我们将这些启发式方法实现到两个开源模型检验工具中，IC3Ref和SimpleCAR，以及成熟的nuXmv平台，并在HWMCC基准测试上进行了广泛的实验评估。结果表明，提出的启发式方法可以有效计算更多的i-good引理，从而提高了上述所有模型检验工具的性能。

董明凯

上海交通大学

上海交通大学并行与分布式系统研究所(IPADS）助理研究员，主要研究方向为操作系统、文件与存储系统，DNA存储，对新型持久内存和新型文件系统设计有深入的研究，相关工作发表在 FAST、USENIX ATC、SOSP 等操作系统顶级国际会议，TreeSLS工作获SOSP2023最佳论文奖，高性能持久内存文件系统 SoupFS 进入 OpenEuler 创新版，与华为合作的 EROFS 被合入 Linux 主线，并已经成为 Android 系统分区的官方文件系统。

报告题目：

TreeSLS：基于持久内存和树形状态的全系统持久化微内核系统

报告摘要：

全系统持久化可以简化应用开发，并具备接近即时恢复的能力。现有全系统持久化系统周期性地为系统状态创建检查点，并保存到持久设备中，这导致较大的持久化性能开销大且无法高效保证外部同步性。本报告将介绍如何结合新兴持久内存与微内核中的树形对象状态简化和降低全系统持久化的性能开销，并通过高频率的持久化支持高效且透明的外部同步性。在微基准测试和Memcached、Redis等真实应用程序中，TreeSLS 可以在 200 微秒内完成整个系统的持久化，同时，在每毫秒进行一次的高频检查点创建下，TreeSLS可以达到与真实应用程序的原生持久化支持相当或更好的性能。

葛季栋

南京大学

葛季栋，南京大学副教授/博士生导师，师从吕建院士，2007年毕业于南京大学计算机系，获博士学位，CCF高级会员、CCF系统软件专委、软件工程专委会和服务计算专委会的执行委员，入选江苏省第六期“333高层次人才培养工程”。曾经主持国家重点研发计划课题、国家自然科学基金、江苏省自然科学基金、华为公司合作项目、金桥信息合作项目等多项科研项目。长期从事自然语言处理与智能软件工程、分布式计算与工作流协同、智慧司法等方向和领域的科学研究与软件开发。已经在ACM TOSEM、IEEE TSE、IEEE TMC、IEEE TPDS、IEEE/ACM TNET、IEEE TIP、IEEE/ACM TASLP、ACM TKDD、IEEE TSC、ASE(Springer)、Inf. Sci.、JSS、JPDC、ComNet、FGCS、JNCA、ESA、ExpSys、JSEP、SCIS、计算机学报、软件学报、电子学报等国内外期刊和ICSE、FSE、ASE、AAAI、EMNLP、IWQoS等重要国际会议上录用和发表论文100余篇。作为核心成员荣获2021年中国电子学会科技进步奖一等奖，作为指导老师曾经荣获ASE2023和MSR2023杰出论文奖（ACM SIGSOFT Distinguished Paper Award），作为主要参与人曾荣获2009/2014年高等教育国家级教学成果奖二等奖、2021年全国优秀教材（高等教育类）二等奖、2018年国家精品在线开放课程《计算机操作系统》、2020年国家一流本科课程《计算机操作系统》、2010年《操作系统原理与实践》国家精品课程。

报告题目：

基于语言模型和解耦数据库的领域自适应代码补全

报告摘要：

代码大模型在代码补全方面表现出了显著性能。但是，在代码大模型补全特定领域内的代码（例如补全项目内私有方法）时，由于代码大模型缺少特定的领域知识，可能并不能正确地补全代码。同时，部分代码大模型的黑盒特性，以及代码所在领域的持续迭代特性，使得为特定领域微调大模型，让大模型自身学习代码领域知识不是一个最佳的解决方案。为此，我们提出了一种检索增强的语言模型，kNM-LM，不通过微调技术，就可以将特定领域知识融入代码大模型中。具体来说，我们将代码领域知识存储到额外的数据库中。在补全时，利用贝叶斯推断来结合大模型和数据库两者的推测能力，最后给出综合的代码补全推荐。我们在不同领域的代码补全数据上验证了kNM-LM的性能。实验证明，kNM-LM在两种代码模型（CodeGPT以及UniXcoder）上都取得了有效的补全性能提升。此外，kNM-LM不需要访问模型内部参数，因此可以与一些黑盒代码大模型结合在一起，集成到现有代码补全插件中。

曾霞

西南大学

博士，现任西南大学讲师。主要研究方向: 智能系统安全控制、信息物理系统分析与验证、可信人工智能、优化理论和符号-数值混合计算等。主持国家自然基金青年项目1项、教育部产学合作协同育人项目1项，参与主研国家自然科学基金面上项目3项。研究论文发表于AAAI、 CAV、 DAC、EMSOFT、HSCC等领域知名国际会议和《Science China Information Sciences》、《软件学报》、《Formal Aspects of Computing》等期刊。

报告题目：

面向可达规避约束的非线性系统组合控制器生成

报告摘要：

对于安全攸关控制系统，如何面向安全性/可达性需求生成具有形式化保障的控制策略，是一个至关重要和亟待解决的研究问题。强化学习技术将系统需求编码为奖励函数进而训练神经网络控制器，在实际控制任务中展现了良好的效果，但如何利用强化学习技术生成满足安全性/可达性规约并且可形式化证明正确性的控制器仍然是一个重大挑战。本文尝试设计、生成和验证一种特殊的“多项式+神经网络”组合形式控制器，该控制器能够更有效地进行形式化验证，同时不失控制能力上的灵活性。本文首先精心设计了一种组合控制器合成的框架，包括强化学习大网络训练、大网络低次多项式拟合、残差小网络模型蒸馏、组合控制器重训练四个阶段；然后将安全/可达验证问题编码为障碍证书和类Lyapunov函数存在性问题，并基于组合控制器的特殊形式最终转化为多项式约束优化问题来求解。论文对一系列基准案例进行了详细的实验评估以展示组合式控制器合成方法的有效性，并通过消融实验表明这种组合式设计的必要性。

林子熠

阿里云

CCF系统专委会执行委员，获得ACM SIGSOFT 杰出论文奖（2023 ICSE）。目前就职于阿里云JVM团队，主要工作在Java native编译和静态分析的开发和应用方向，出版《GraalVM与Java静态编译原理与应用》一书。参与的开源社区工作包括：GraalVM社区贡献者，Apache Committer，龙蜥社区机密计算SIG maintainer。

报告题目：

Lejacon：一种轻量高效的用于SGX硬件的Java机密计算方法

报告摘要：

机密计算是一种硬件隔离保护程序运行时的技术。它将安全敏感的数据和程序置于硬件加密隔离的可信运行时环境（TEE）中，TEE之外的任何程序都无法获取其中的数据和信息。典型的硬件设备有Intel在X86平台的SGX。目前机密计算的硬件上只支持运行native程序，所以庞大的Java生态并不能方便地享受到机密计算带来的安全红利。本文提出了一种轻量级的分离编译技术，支持用户开发Java的机密计算应用。实验证明，LeJacon可以有效防御Log4J的注入攻击。LeJacon已在Apache开源，目前正处于项目孵化中。

糜泽羽

上海交通大学

上海交通大学助理研究员，硕士生导师，主要从事操作系统和系统虚拟化的研究，主持国家自然科学基金面上项目、青年基金项目等国家级科研项目。在SOSP、 OSDI、 ASPLOS、EuroSys、USENIX Security、IEEE TC等操作系统顶级会议和期刊发表十余篇学术论文。

报告题目：

DuVisor：软硬协同的用户态虚拟机监控器

报告摘要：

目前主流的系统虚拟化系统由两个部件组成：一个是使用硬件虚拟化的内核驻留程序，一个是提供虚拟机管理和I/O虚拟化的用户态进程。然而，这种虚拟化架构在安全性和性能方面都存在问题。此前的相关工作通过将内核功能卸载到用户态的方式最小化内核的部分，这种设计却面临着安全和性能之间的权衡：虽然更多的卸载可能会减少内核的攻击面，但却增加了内核态与用户态之间的模式切换，从而增加了虚拟化系统的性能开销。本次报告将介绍一种软硬件结合的新型虚拟化系统设计，它将内核驻留程序参与的控制平面与用户态进程的数据平面完全分开，从而消除了内核在虚拟机运行时的干预。基于这种设计而实现的用户态虚拟机监控器DuVisor，可以直接在用户态处理几乎所有的虚拟机下陷，包括在用户态配置虚拟机寄存器，管理第二阶段页表并实现高效的I/O虚拟化。我们已经在一个开源的RISC-V CPU上实现了硬件扩展，并构建了基于Rust的虚拟机监控器。在FireSim平台上的评估数据显示，DuVisor给应用带来的开销低于5%。