Welcome to the SQuARE Research Group

The group conducts in-depth research on static analysis techniques for C/C++, providing high-precision static analysis solutions for underlying system software and embedded systems written in C/C++.

• Canalyze / Canalyze++ Utilizes static symbolic execution technology to inspect C/C++ code, automatically discovering potential defects and vulnerabilities that could lead to crashes or serious errors. The tool supports 14 types of CWE errors and 2 other error types, capable of concurrent analysis of large-scale C/C++ programs. Analyzed projects include, but are not limited to, OpenHarmony, MySQL, and PostgreSQL. It has discovered and reported over a hundred real-world defects in open-source and enterprise cooperative projects.
• Crulet A checking tool developed for rules in programming standards such as GJB 8114—2013 “Safety Subset for C/C++ Language Programming”. It is based on syntax tree matching and flow-sensitive global analysis. It ensures analysis accuracy while maintaining execution efficiency, achieving over 90% accuracy on rules requiring high-precision analysis, such as memory leaks. It has discovered and reported over four hundred real-world defects in open-source and commercial applications.

The group deeply investigates static analysis techniques for Java programs, resulting in Justin, a unit test case generation tool for Java. Its main features include:

• Support for various Java features Supports polymorphism, inheritance, generics, and tests for data structures and design patterns like arrays, collections, and singletons.
• Applicable to diverse business scenarios Specifically designed and optimized for string generation in complex API calls, sparse input spaces in business data, and the explosion problem of full combinatorial coverage.
• Support for multiple test data generation strategies Supports strategies such as random, special value, white-box, annotation-based, and combinatorial generation, showing good performance in coverage, distribution, and defect detection capability.
• Discovery of numerous real defects The tool has discovered and confirmed 24 defects in the open-source community (including 14 in the JDK) and accumulated 1,731 valid defects in real-world enterprise applications.

The group focuses on mobile application quality assurance, addressing pain points such as chaotic resource management, misuse of asynchronous components, and insufficient automated test coverage by providing solutions for static defect detection, automated testing, and fault localization.

• Resource Leak / Asynchronous Component Misuse Detection Targeting the use of high-energy hardware resources and asynchronous components, this solution analyzes API calling patterns and error modes. Using lightweight inter-procedural analysis technology, it detects issues like erroneous page updates, abnormal battery consumption, and crashes caused by resource leaks. It has found over a hundred real defects in well-known open-source projects, map, and e-commerce commercial apps, which were confirmed and fixed by development teams.
• Automated Testing and Fault Localization The group developed a series of automated analysis and testing tools for mobile apps, including Fax, ICCBot, and ICTDroid. These support constructing various startup contexts, achieving multi-entry automated exploration, and precise localization of framework-layer crash errors. Related technologies have discovered multiple real defects in open-source apps and some AI-related enterprise apps, confirmed and fixed by development teams.
• HarmonyOS Native Testing Developed the hmbot automated testing framework, combining static analysis with reinforcement learning to achieve efficient exploration and testing of HarmonyOS applications. Addressing the unique cross-device transfer scenarios of HarmonyOS, the HACMony tool was developed, discovering over 50 new types of distributed defects related to resource transfer conflicts in over 10 domestic mainstream audio/video commercial apps.

The rapid development of large model technologies in recent years has injected new vitality into software engineering tasks. Building on long-term research in software analysis and defect detection, the group is actively exploring intelligent code inspection empowered by large models, conducting in-depth research on both traditional static analysis inspection and AI agent-based inspection.

• Automatic Generation of Static Code Checkers To meet the customized code inspection needs of different enterprise projects, the group proposed the AutoChecker method. By providing code inspection rule descriptions and corresponding positive/negative example sets, this method automatically generates static code checkers for the rules. Currently supporting automatic generation for Java and C/C++ code, it focuses on inspection needs based on code syntactic structure pattern matching.
• Construction of Code Inspection AI Agents Developed a method for constructing AI agents for code inspection oriented towards defect reports. Given a defect report or issue ticket to be checked, this method first generates corresponding intelligent inspection rules, then builds an AI agent based on these rules to detect similar defect issues through a three-stage process: “entry point localization — context extraction — defect judgment”.

Autonomous driving systems operate in highly complex environments, dealing with diverse road structures and the dynamic behaviors of surrounding traffic participants. The group proposes testing and simulation verification methods for autonomous driving systems.

• Critical Configuration Testing Proposed the CCTest method, which identifies the capability and responsibility boundaries of autonomous driving systems based on constraint analysis. Using criticality sorting, it generates the most extreme test cases within these boundaries. This method has been applied to the Baidu Apollo open platform, assisting in the discovery of multiple accident scenarios, and won the Second Prize in the Prototype System Competition at the 2025 China Software Conference.
• Simulation Verification By constructing a simulation verification system based on semantic models, it effectively compensates for the lack of controllability and observability in road testing, achieving systematic safety and performance verification of autonomous driving algorithms under diverse environmental conditions. It supports testing of 8 types of autonomous driving systems on Carla or LGSVL simulation platforms, discovering safety or performance defects in all 8 systems.

As the group’s traditional strength and core technological foundation, we are committed to tackling the “hard nuts” in automated reasoning and constraint solving technologies.

• Core Technology Focusing on Satisfiability (SAT/SMT) problem solving, leading internationally in Volume Computation and Model Counting (#SMT) of the solution space.
• Theoretical Breakthroughs Proposed efficient volume estimation and exact counting algorithms for Boolean combinations of linear arithmetic constraints and non-linear constraints. Related work on non-linear integer constraint solving won the ISSTA 2023 Distinguished Paper Award.
• Application Empowerment Providing key quantitative reasoning engines for probabilistic program analysis, software configuration space analysis, and quantitative information flow security. The “Modeling and Algorithm Application for Optimization Scheduling of Shortwave Broadcast Resources,” a collaboration with the Radio Administration of the State Administration of Press, Publication, Radio, Film and Television, won the First Prize of the “Wang Xuan News Science and Technology Award” from the China Association of News Technicians.