新闻
了解我们最新的公告和研究亮点
张健研究员获 QRS 二十五周年特别荣誉奖（Special Recognition Award）
SQuARE 组员张健研究员，荣获 IEEE 软件质量、可靠性与安全国际会议（QRS）颁发的 “特别荣誉奖”（Special Recognition Award）。该奖项为 QRS 会议二十五周年特别设立，旨在表彰在过去 25 年中，于 QRS 发表多篇论文并为软件质量研究与应用做出重要贡献的学者。根据 QRS 组委会介绍，该奖项旨在肯定张健研究员在程序分析和测试数据生成领域发表于该会议系列（包括其前身 QSIC、SERE 和 APAQS）的工作。 组委会引述的具体贡献包括： + APAQS 2000 & IJSEKE 2001: 发表关于通过求解布尔与数值组合约束进行规约分析与测试数据生成的论文，并介绍了其 BoNuS 工具。 + APAQS 2001: 提出了一种用于检测无限循环的路径分析方法，为程序不终止问题建立了一个充分条件。 + QSIC 2006: 与其博士生许中兴共同开发了一款 C 语言测试数据生成工具，该工具采用符号执行与约束求解技术，在 GNU CoreUtils 等基准测试上达到了高代码覆盖率。 + QSIC 2008: 与许中兴共同提出了一种路径与上下文敏感的跨过程内存泄漏检测技术，并用于在开源软件中发现缺陷。 除研究工作外，组委会也提及了张健研究员为会议提供的服务。他曾担任 QSIC 2003 的组织委员会联合主席、QRS 2015 的程序委员会联合主席，并任 SERE 2014 的主旨演讲嘉宾，同时多次担任 QRS/QSIC 程序委员会委员。
张健、严俊研究员荣获中国科学院大学2025年“教育教学成果奖”一等奖
近日，中国科学院大学公布了 2025 年度 “教育教学成果奖” 评审结果。中国科学院软件研究所（ISCAS）推荐的教育教学项目 “面向国家需求的集成式本硕博贯通软件人才培养体系创新与实践” 荣获一等奖。 该项目由软件所张健研究员担任团队负责人，主要成员包括国科大计算机科学与技术学院沈海华教授，以及软件所魏峻研究员、严俊研究员和蔡少伟研究员等。值得一提的是，张健研究员和严俊研究员均为 SQuARE 组成员。本项目采用 “全栈式智能化教学平台 + 开源生态” 的教育教学模式，构建了 “基础理论学习→编程实践→工业化软件开发实战” 三阶段贯通培养体系，推行以重要科研项目为驱动的科教融合创新实践。该团队的教育教学方式和科研成果在国内外产生了积极影响，培养的学生取得了一系列科研成果，荣获多项荣誉。 
傅艺玄同学获评国科大校级优秀本科毕业论文
近日，中国科学院大学公布了2025届校级优秀本科生毕业论文（设计）推荐名单，计算机科学与技术专业共有8篇论文入选，傅艺玄同学的毕业论文成功入选其中。 傅艺玄的论文题为《基于动态反馈的深度学习库组合测试方法》，由严俊研究员指导。该研究针对深度学习库测试中的一个常见问题：当一个测试用例因特定参数组合违背约束而崩溃时，传统的组合测试方法会错误地将该用例中其他未被执行到的参数组合也标记为“已覆盖”，即“伪覆盖”问题。 为解决该问题，论文提出了一种基于动态反馈的组合测试方法。该方法通过分析程序崩溃的直接反馈来提取导致问题的核心参数组合，并以此为依据补充生成新的测试用例，从而实现对参数组合更真实的覆盖统计和更全面的测试。该项研究工作以 Keras 深度学习库作为测试对象完成了实验验证。 
黄沛博士荣获 “CCF 博士学位论文激励计划” 提名
2024 年 1 月 27 日，2023 年 CCF 颁奖大会暨理事长就职典礼在北京召开。大会为入选和提名 2023 年 “CCF 博士学位论文激励计划” 的博士颁发了获奖证书。2022 届毕业生黄沛博士（导师：张健教授）凭借其博士学位论文《逻辑公式可满足性判定中的推理技术研究》获得该计划提名。 黄沛博士现为美国斯坦福大学计算机系博士后，其博士论文聚焦于逻辑公式可满足性判定这一计算机核心问题，提出了两种混合推理框架以提升自动推理效率，并基于此攻克了若干组合数学难题，取得了多项创新性成果。论文相关结果已被《Handbook of Satisfiability》和《Handbook of Combinatorial Design》收录。论文还提出了模态逻辑 S5 系统中的新范式及推理规则，显著提升了 S5 自动推理工具的效率，并被国际同行采纳。此外，论文将逻辑推理技术应用于深度学习系统的软件理论，提出了𝜀- 弱鲁棒性概念及神经网络鲁棒性增强方法。 “CCF 博士学位论文激励计划” 旨在激励计算机领域博士研究生潜心钻研、务实创新，表彰在计算机领域取得优秀成果的青年学者。2023 年共有 9 篇论文入选该激励计划，5 篇论文获得提名。
燕季薇博士的博士学位论文入选中国计算机学会软件工程专业委员会2023年度“博士学位论文激励计划”
燕季薇博士（指导教师：严俊研究员）的博士学位论文《基于框架与应用协同分析的安卓应用质量保障技术研究》入选中国计算机学会软件工程专业委员会2023年度“博士学位论文激励计划”。其论文关注基于复杂编程框架的移动应用程序质量保障自动化技术，采用字节码静态分析技术提取框架代码信息，基于框架信息开展上层应用分析测试，有效解决了复杂框架特性导致的上层应用缺陷难以被触发、重现和定位等问题。 “博士学位论文激励计划”是由CCF专业委员会设立，旨在进一步推动软件领域高水平创新人才培养工作。该计划评选采用推荐-评审制，由单位推荐或CCF会员联名推荐候选博士学位论文，各专业委员会组建的计划评审委员会组织评审，评选过程具体包括推荐、资格审查、初评、终评四个阶段。各专业委员会每年评选出不超过3篇，在相关领域做出杰出创新研究工作的博士学位论文，对论文完成人给予表彰和奖励。
《软件测试与分析》课程获评国科大2023年校级“本科生优秀课程”
近日，2023年中国科学院大学校级“本科生优秀课程”评选名单公布，由软件所开设的计算机专业选修课——《软件测试与分析》名列其中。 《软件测试与分析》自2017年秋季学期开始面向高年级本科生（大三、大四）开设，虽为计算机软件方向的选修课，但不限制选课学生的专业。课程注重通过实践使学生掌握真实应用测试场景中常用的测试方法，了解基本的程序分析技术，并能够运用1至2种前沿的程序分析与测试技术自动化工具解决真实世界的问题。课程选取趣味性强的哥德尔编码器、游戏寻路算法、房价计算器、流行的GitHub开源项目等程序作为测试对象，帮助学生理解运用课堂知识，体验真实的bug发现过程。该课程的教案还获得了北京市教育委员会评选的“优质本科教案”奖。 课程授课团队成员为来自 SQuARE 课题组的严俊研究员、张健研究员和燕季薇助理研究员。授课团队长期从事程序分析与测试领域的科研和教学工作，2023年度荣获了中国科学院大学“领雁奖银奖·振翅奖”。
SQuARE 组非线性整数约束求解研究工作获 ACM SIGSOFT 杰出论文奖
近日，SQuARE 组博士生贾富琦、马菲菲研究员和张健研究员，与中国科学院软件研究所计算机科学国家重点实验室、并行软件与计算科学实验室合作完成的论文《Improving Bit-Blasting for Nonlinear Integer Constraints》被软件工程领域顶级国际会议 ISSTA（International Symposium on Software Testing and Analysis）接收，并荣获 ACM SIGSOFT 杰出论文奖（ACM SIGSOFT Distinguished Paper Award）。 该论文针对非线性整数约束的求解，提出了一种基于位展开（Bit-Blasting）方法的求解框架，涵盖了搜索空间的预处理和位展开最优加和顺序的算法。团队自主研发并实现了 SMT 求解器 BLAN，在可满足实例求解性能上显著优于目前主流 SMT 求解器（如微软的 Z3、斯坦福与爱荷华大学的 CVC5 等）。 可满足性模理论 (SMT) 是自动推理的一个重要领域，它研究在某些特定理论（如：算术理论、数组理论等）下的一阶逻辑公式的可满足性的判定方法。而非线性整数约束则是其中一类常见且困难的约束类型，常出现在规划、软件 / 硬件验证和分析、自动化测试等实际问题中。在 SMT 中，一类经典的方法是通过位展开 (Bit-Blasting) 将非线性整数约束转化为对应的布尔可满足性问题进行求解。 通过观察和实践，团队发现目前主流的算法设计存在着诸多问题。针对这个现状，论文提出了一系列优化策略，显著提升了求解效率。针对搜索域难以确定的问题，论文提出了应对非线性乘法和特定约束的确定位长的启发式策略，以寻找到合适的搜索空间。针对连续加法中不同顺序导致冗余的问题，论文提出了一个最优顺序决策算法并证明了其最优性。详细的消融实验验证了所提方法的有效性。 此外，团队还进一步探究了位展开方法求解不可满足实例的实现路径。
张健、严俊研究员获 2021 年度 CCF 科学技术奖自然科学一等奖
2021 年 12 月 17 日，在中国计算机大会（CNCC2021）期间，中国计算机学会（CCF）举行了年度颁奖典礼。中国科学院软件研究所与中国人民大学合作完成的成果 “高精度智能化的软件分析与测试方法” 荣获 2021 年度 CCF 科学技术奖自然科学一等奖。其中 SQuARE 组张健研究员、严俊研究员是主要完成者之一。 本项目针对软件分析与测试领域中的精度、知识获取难题，以及移动计算和人工智能带来的新需求，从静态分析效能提升、组合测试、模糊测试、并发测试等多个角度出发，显著提高了软件分析与测试方法的精度和智能化水平。相关研究成果不仅在学术界产生重要影响，也被应用于实际工业项目，有效发现了多个著名开源软件和软件产品中的缺陷。 “CCF 科学技术奖” 旨在授予在计算机科学、技术或工程领域具有重要发现、发明、原始创新，在相关领域有一定国际影响的优秀成果。会议还颁发了 CCF 王选奖、CCF 海外杰出贡献奖、CCF-ACM 人工智能奖、CCF-IEEE CS 青年科学家奖。 
张健研究员团队参与获得 2021 年度国家自然科学基金重点项目资助
2021 年 8 月 18 日，国家自然科学基金委员会公布了 2021 年度国家自然科学基金评审结果。中国科学院软件研究所获得多项资助，其中由 SQuARE 组张健研究员牵头申报的 “面向形式化验证的可信编译和程序分析” 项目获得国家自然科学基金重点项目资助。 张健研究员长期致力于自动推理、约束求解、程序静态分析与检错、软件测试数据生成等方向的研究，并担任多项国内外权威学术期刊编委。此次重点项目将围绕程序分析和加固技术的验证、语义增强的程序分析、面向形式验证的程序化简、形式规约的检查等方面开展深入研究。
张健研究员当选 CCF 会士
2018 年度 CCF 会士评选会在学会总部举行。2018 年度共收到会士候选人提名材料 15 份，2018 年度 CCF 会士评选委员会委员仔细审阅了提名材料，经过讨论和无记名投票，七位 CCF 杰出会员当选 CCF 会士。中国科学院软件研究所 SQuARE 组张健研究员成功当选。  张健研究员主要研究方向包括自动推理、约束求解、软件测试与分析。现担任《计算机学报》、JCST、Frontiers of CS、IEEE Trans. on Reliability、《中国科学》、《计算机科学与探索》等期刊编委，国家 973 计划项目 “安全攸关软件系统的构造与质量保障方法研究” 首席科学家。曾获中创软件人才奖、国家杰出青年科学基金。现任 CCF 学术工委执行委员、公共政策委员会执行委员、专委工委委员，积极参与 CCF 推荐国际学术会议 / 刊物目录审查与修订，代表学会参加专委会会议；作为 CCF 形式化方法专委和软件工程专委委员，承担专委学术会议和学科发展报告撰写等工作。 CCF 设立会士制度旨在表彰在计算机领域取得卓越成就或为 CCF 做出突出贡献并有连续五年以上会籍的 CCF 会员。会士是会员在 CCF 的最高学术荣誉。