欢迎来到 SQuARE 课题组
SQuARE (Software Quality and Automated REasoning) 课题组隶属于中国科学院软件研究所。在张健研究员的带领下，课题组长期致力于程序分析、软件测试、自动推理和约束求解等领域的基础与应用研究。 课题组坚持理论创新与工具落地并重，近年来在 ICSE, FSE, ASE, ISSTA (软件工程顶会) 及 NeurIPS, AAAI (人工智能顶会) 等高水平会议和期刊上发表了大量学术成果，并承担了多项国家级重大科研项目。课题组现有职工 11 人，其中研究员 3 人，副研究员 2 人，高级工程师 1 人，工程师 3 人，博后 2 人。
C/C++ 软件分析及缺陷检测
课题组深入研究 C/C++ 程序静态分析技术，针对采用 C/C++ 语言编写的底层系统软件与嵌入式系统等，提供高精度的静态分析解决方案。
- Canalyze / Canalyze++ 使用静态符号执行技术对 C/C++ 代码进行检测，并自动发现程序中潜在的可能导致程序崩溃或严重错误的缺陷和漏洞。工具支持 14 种 CWE 错误和 2 种其它错误，支持对大规模 C/C++ 程序的并发分析，曾分析过的项目包括但不限于 OpenHarmony、MySQL、PostgreSQL 等。在开源和各类企业合作项目中累计发现并报告百余项真实缺陷。
- Crulet 针对 GJB 8114—2013《C/C++ 语言编程安全子集》等编程标准中的规则，基于语法树匹配和流敏感的全局分析方法研发的检查工具。在保证运行效率的同时有较准确的分析能力，在内存泄漏等需要高精度分析的规则上达到 90% 以上准确率，在开源和商业应用上累计发现并报告四百余处真实缺陷。
Java 软件分析与测试
课题组深入研究 Java 程序静态分析技术，形成面向 Java 程序的单元测试用例生成工具 Justin。该工具主要具有以下特点：
- 支持各类 Java 特性 支持 Java 的多态、继承、泛型等语言特性，支持对数组、集合、单例等数据结构和设计模式的测试。
- 适用各类业务场景 工具对复杂 API 调用的字符串生成、稀疏的业务数据输入空间和全组合覆盖的爆炸问题等进行了针对性设计和优化。
- 支持多种测试数据生成策略 支持随机、特殊值、白盒、注解和组合等测试数据生成策略，覆盖率、分布情况和缺陷检测能力表现良好。
- 发现大量真实缺陷 工具在开源社区上发现并确认 24 处缺陷（包含 JDK 中 14 处），企业真实应用中累计发现 1,731 处有效缺陷。
移动应用分析与测试
课题组深耕移动应用质量保障领域，针对移动应用中的资源管理混乱、异步组件误用及自动化测试覆盖不足等痛点，提供静态缺陷检测、自动化测试及错误定位解决方案。
- 资源泄露／异步组件误用检测 针对高能耗硬件资源和异步组件的使用，通过分析相关 API 的调用方式与错误模式，采用轻量跨过程分析技术，检测资源泄露导致的页面错误更新、电量异常消耗与程序崩溃等问题。曾在知名开源项目、地图类和电商类商业应用中发现百余处真实缺陷，并获开发团队确认与修复。
- 自动化测试与错误定位 课题组研发的一系列移动应用自动化分析和测试工具 Fax、ICCBot 和 ICTDroid 等，支持构造各类启动上下文，实现移动应用多入口自动化探索，并支持框架层崩溃错误的精准定位。相关技术在开源应用和部分 AI 相关企业应用上发现多种真实缺陷，并获开发团队确认与修复。
- 鸿蒙原生测试 研发 hmbot 自动化测试框架，结合静态分析与强化学习技术，实现对鸿蒙应用的高效探索与测试。针对鸿蒙特色的跨端流转场景，研发 HACMony 工具，在 10 余个国内主流音视频商业 APP 中发现 50 余处资源流转冲突类新型分布式缺陷。
智能化代码检查
近年来大模型技术的飞速发展为软件工程各任务注入了新活力，课题组在已有的长期软件分析与缺陷检测研究基础上，也积极探索大模型赋能下的智能化代码检查，针对传统静态分析检查以及 AI 智能体检查都开展了深入研究。
- 静态代码检查器自动生成 为了满足实际不同企业项目的定制化代码检查需求，课题组提出 AutoChecker 方法，用户提供代码检查规则描述以及相应规则正反例集，本方法即可自动生成针对该规则的静态代码检查器。该方法目前支持针对 Java、C/C++ 代码的静态检查器自动生成，重点面向基于代码语法结构模式匹配的代码检查需求。
- 代码检查 AI 智能体构建 研制面向缺陷报告的代码检查 AI 智能体构建方法。给定需要检查的缺陷报告或者问题单，本方法首先生成相应的智能化检查规则，进而基于该智能化规则构建 AI 智能体，通过“入口点定位—上下文提取—缺陷判断”三阶段检测其它类似缺陷问题。
自动驾驶
自动驾驶系统运行于高度复杂的环境中，既要应对多样化的道路结构，也要处理周边交通参与者的动态行为。课题组提出针对自动驾驶系统的测试与仿真验证方法。
- 关键配置测试 提出 CCTest 方法，基于约束分析识别自动驾驶系统的能力边界与责任边界，并基于关键性排序，生成边界内最极端的测试用例。该方法已应用于百度 Apollo 开放平台，协助发现多种事故场景，获 2025 年中国软件大会原型系统竞赛二等奖。
- 仿真验证 通过构建基于语义模型的仿真验证体系，有效弥补道路测试中可控性与可观测性不足，实现对自动驾驶算法在多样化环境条件下的系统性安全与性能验证。已支持 8 种自动驾驶系统在 Carla 或 LGSVL 仿真平台中的测试，发现全部 8 种自动驾驶系统安全或性能缺陷。
自动推理与约束求解
作为课题组的传统强项与核心技术底座，致力于攻克自动推理与约束求解技术中的“硬骨头”。
- 核心技术 关注可满足性 (SAT／SMT) 问题求解，在解空间体积计算 (Volume Computation) 和 解计数 (Model Counting/#SMT) 方面处于国际前沿。
- 理论突破 针对线性算术约束及非线性约束的布尔组合，提出高效的体积估算与精确计数算法。相关非线性整数约束求解工作成果获 ISSTA 2023 Distinguished Paper 奖项。
- 应用赋能 为概率程序分析、软件配置空间分析及定量信息流安全提供关键的量化推理引擎，与国家新闻出版广电总局无线电台管理局合作的成果“短波广播资源优化调度建模及算法应用”获中国新闻技术工作者联合会“王选新闻科学技术奖”一等奖。