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

nbsp; +

+

论坛巡礼

论坛名称：顶会顶刊论坛

时间: 2022年11月25日上午8:30-17:40

论坛简介：

        2022年度顶会顶刊论坛邀请了复旦徐辉副研究员、武大谢晓园教授、南大潘敏学副教授、南大冯洋助理研究员、南方科大张煜群助理教授、北京理工张宇霞副研究员、上海交大王肇国副教授、华科张宇副教授、浙大姚培森研究员、华师大刘静教授和上海交大许智磊副教授等11位知名学者分别就各自的优秀成果做宣讲 告。本论坛今年还邀请到天津大学陈俊洁研究员以及南大卜磊教授作特邀 告。

        热烈欢迎各位通过扫描下方二维码提前提问，以便论坛嘉宾更有针对性地进行讨论和解答。

张天

博士、教授、博士生导师

   主要研究领域为智能化软件工程、模型驱动软件技术等，研究成果发表在国际重要会议和期刊50余篇（包括TSE、TOSEM、ICSE、FSE、ASE等），获ISSTA杰出论文奖。主持国家自然科学基金青年、面上项目，参与多个国家重点、重大科研项目。相关研究成果获发明专利授权20余项，多项成果已应用在华为、腾讯（微信）、OPPO等国内领头企业中。

刘辉

北京理工大学计算机学院教授、CCF 杰出会员、软件工程专委会常务委员

告及讲者

Reports and reporters

徐辉

复旦大学计算机科学技术学院青年副研究员、香港中文大学博士

    专注程序分析、软件测试等软件系统可靠性分析和评价技术研究，已在该领域的顶级国际学术会议和期刊发表多篇学术论文，并获得ACM SIGSOFT优秀论文奖。详见个人主页：https://hxuhack.github.io。

告题目：

基于静态分析的Rust内存安全缺陷检测研究

告摘要：

    Rust语言是近年来快速兴起的一门以内存安全著称的系统级编程语言。但是，当前的Rust语言设计依然存在诸多不足。本次 告将探讨Rust语言的安全机制、实用效果和设计缺陷，并重点介绍我们在TOSEM（ASE 2022 Journal-first Track）发表的一篇工作。该工作聚焦Rust语言的自动内存回收机制对其内存安全防护产生的副作用，即可能导致悬空指针问题。针对该问题，我们提出了一套路径敏感的悬空指针缺陷检测方法，并通过实验证明该方法可以达到较高的准确性和效率。

潘敏学

南京大学软件学院副教授、博导、CCF系统软件专委会执行委员

告题目：

面向带噪声和类别不平衡软件数据的鲁棒深度预测模型的学习方法研究

告摘要：

    在本 告中，我们将介绍能在原始软件数据集上进行深度预测模型的鲁棒学习方法RobustTrainer。RobustTrainer通过一个创新的两阶段训练方案，首次实现了对存在样本噪声和类别不平衡共存问题的软件数据的鲁棒学习。第一阶段学习对样本噪声问题鲁棒的特征表示，第二阶段基于第一阶段学习的表示，构建对类别不平衡问题鲁棒的分类器。在错误 告分类和软件缺陷预测两个软件工程任务上的实验结果表明，与其他主流的鲁棒学习方法相比，RobustTrainer产生了更优的深度预测模型。

张煜群

南方科技大学计算机科学与工程系助理教授

研究工作集中在包括模糊测试、污点分析、代码预训练模型等领域。他在包括TSE, TOSEM, TPDS, ICSE, ISSTA, ASE, DAC等相关领域国际期刊会议上共发表论文三十余篇，并在ISSTA’19上获得ACM SIGSOFT杰出论文奖。

告题目：

One Fuzzing Strategy to Rule Them All

告摘要：

卜磊

南京大学软件学院教授、博导

主要研究领域是软件工程与形式化方法，包括模型检验技术，实时混成系统，信息物理融合系统等方向。2010年在南京大学获取计算机博士学位。曾在CMU、MSRA等科研机构进行访学与合作研究。相关工作发表于领域重要期刊与会议如TCAD、TC、TDSC、TCPS、TPDS、RTSS、HSCC等。入选国家级青年人才计划，NASAC青年软件创新奖，高校计算机专业优秀教师奖励计划，CCF青年科技奖等。

告题目：

基于分类模型无梯度优化的复杂系统测试生成

告摘要：

    随着科技的快速发展，软件系统复杂度急剧提升，对相关软件系统的质量保障愈发重要也愈发难以进行。本 告对我们近期将基于分类模型无梯度优化算法应用到复杂软件系统分析与测试中的相关探索与尝试做一个简要介绍。首先，我们在软件代码符 执行中将包含非线性运算、第三方函数调用等难以求解的约束可满足问题转换成无梯度优化问题，使用猜测-验算-反馈-学习机制来对约束可行解进行反向学习而不是正向求解，从而实现含相关复杂路径约束的代码符 执行。在上述工作的启发下，我们进一步将相关技术应用到实时混成系统测试与控制生成，乃至深度学习 络对抗样本生成等多个问题中，将不同领域的难解问题统一抽象成为搜索/最优求解问题，并转化为优化问题，继而采用上述猜测-验算-反馈-学习机制进行有效求解。

张宇

华中科技大学副教授、博士生导师

CCF高级会员，CCF高性能专委会委员、CCF体系结构专委会委员，之江实验室特聘专家，2016年6月在华中科技大学获得计算机系统结构博士学位，主要研究高性能计算、体系结构和系统软件、图计算，主持国家自然科学基金和企事业项目10余项，参与国家重点研发计划项目、国家自然科学基金重点基金、863计划课题等，在ISCA、ASPLOS、HPCA、SC、DAC、USENIX ATC、ACM TOS、ACM TACO、IEEE TPDS、IEEE TC等CCF A/B类和IEEE/ACM Transactions上发表学术论文58篇，获评CCF A类会议USENIX ATC 2018最佳存储相关论文和最佳论文提名，入选国际顶级期刊IEEE TC的Featured Paper of the Month和ACM TACO的Five Recent TACO Articles of Interest等，相关成果被科技日 （头版）、科学 （要闻）、人民日 等 道。

告题目：

拓扑驱动的动态图计算优化

告摘要：

    现实世界的图通常随着时间动态改变，该类型的图被称为动态图。为有效支持动态图处理，大量动态图处理系统采用增量计算的方式来快速获得最新图快照的计算结果。然而，在对动态图的每个图快照进行处理时，受图更新影响的图顶点最新状态值会沿着图拓扑非规则传递，导致现有方法面临着严重冗余计算和不规则内存访问问题。本 告将探讨拓扑驱动的动态图计算优化技术，高效解决上述问题。具体来说，该技术通过高效规则化动态图处理中受影响的图顶点状态传递和提高数据访问局部性，从而有效减少冗余计算和数据访问开销，保证动态图处理应用在众核处理器上的高效计算。

刘静

华东师范大学软件工程学院教授、博导

“教育部可信软件国际联合实验室”主任，法国爱斯特尔公司（Esterel Ltd.）- 华东师范大学的“模型驱动式轨交软件研发联合实验室”主任。“基于模型的可信软件理论与开发方法”获“教育部自然科学一等奖”。主要研究模型驱动式安全攸关系统构造理论及技术，包括高可信系统构造方法、软件建模语言、模型转换、模型精化与模型验证。研究保证动态模型与静态模型之间的一致性，和基于证明义务的模型精化策略，以及降低系统验证中的空间爆炸可能性问题的理论与实验方法，特别是难以发现的小概率事件的模型检查。在ASE、RTSS、ICSE等学术会议和IEEE Trans. ITS 等学术期刊上发表论文100余。研究成果被法国INRIA、美国CMU等学者等广泛引用。

   与INRIA Sophia Antipolis、INRIA Lyon、Ecole Normale Superieure de Lyon等建立了长期合作关系，于2008 年、2010年、2014年、2017年、2018年、2020年多次赴法国国家信息与自动化研究所 INRIA，在AOSTE实验室进行合作研究，研究了实时系统建模语言、建模规范、模型验证问题。与法国里昂高师Yves Robert教授、INRIA Frederic Vivien研究员、INRIA Robert De Simone研究员等联合培养博士生3名。

    先后主持了国家863项目“模型驱动式高可信软件开发技术”、国家自然科学基金可信软件重大研究计划项目、国家973课题、国家重点研发计划课题、工信部民用飞机专项课题、国家自然科学基金国家合作项目和5项国家自然科学基金面上项目。作为PI参与国家自然科学基金创新群体、上海市产学研协同创新平台建设等。

    在企业应用方面，针对高端核心控制软件可信性难以保障问题，提出的“模型驱动式高可信软件构造方法”，被广泛应用于安全攸关软件系统研发，包括轨道交通无人驾驶系统、飞机发动机系统、飞机显控系统等核心高端软件研发。

告题目：

Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural Networks

告摘要：

    The robustness of deep neural networks is crucial to modern AI-enabled systems and should be formally verified. Sigmoid-like neural networks have been adopted in a wide range of applications. Due to their non-linearity, Sigmoid-like activation functions are usually over-approximated for efficient verification, which inevitably introduces imprecision. Considerable efforts have been devoted to finding the so-called tighter approximations to obtain more precise verification results. However, existing tightness definitions are heuristic and lack theoretical foundations. We conduct a thorough empirical analysis of existing neuron-wise characterizations of tightness and reveal that they are superior only on specific neural networks. We then introduce the notion of network-wise tightness as a unified tightness definition and show that computing network-wise tightness is a complex non-convex optimization problem. We bypass the complexity from different perspectives via two efficient, provably tightest approximations. The results demonstrate the promising performance achievement of our approaches over state of the art: (i) achieving up to 251.28% improvement to certified lower robustness bounds; and (ii) exhibiting notably more precise verification results on convolutional networks.