Yufeng Zhang

Constraint solving remains a fundamental challenge in symbolic execution. To reduce the computational overhead of SMT solvers, modern symbolic execution tools commonly cache and reuse the results of previously solved queries. However, existing caching mechanisms primarily focus on satisfiable queries, offering limited support for unsatisfiable ones, which are still delegated to the underlying SMT solver. To address this problem, we introduce a novel Unsatisfiable Core Guided ( Ucg ) constraint solving framework for symbolic execution. The proposed framework accelerates constraint solving by systematically exploiting unsatisfiable cores, which provide compact explanations for unsatisfiability. Specifically, Ucg first constructs an unsatisfiable core cache with a least-recently-used (LRU) replacement policy to enable the reuse of previously computed unsatisfiable cores. Upon a cache miss, Ucg further exploits the temporal locality of assertions within unsatisfiable cores to predict a potential unsatisfiable core for the pending query. This predicted core serves as an over-approximation of the original query and is likely to be unsatisfiable. By solving this much smaller over-approximated formula, Ucg can infer the satisfiability of the original query with substantially reduced SMT solver effort. We integrated Ucg into Klee , a state-of-the-art symbolic execution tool for C programs. Experimental results on 99 open-source real-world programs demonstrate that Ucg consistently improves the efficiency of both constraint solving and path exploration in symbolic execution across various search strategies. In the best-case scenario, Ucg can achieve improvements of up to two orders of magnitude.

The principled combination of symbolic execution and random testing lacks a formal foundation, especially in deciding which inputs to symbolize. We propose selective concolic testing, a cost-aware framework that formulates this choice as an optimized policy problem of a MDP (Markov Decision Process). We model program exploration over a finite control-flow graph, where MDP states represent covered statements, actions partition path constraints into symbolic and random fragments, rewards reflect coverage gain, and costs account for SMT solving effort and sampling inefficiency. Our framework yields the first formal characterization of selective symbolization as policy synthesis in a probabilistic system. We prove that exact policy computation is intractable due to the exponential state space and the hardness of solution-density estimation via model counting. Our formulation enables a practical approximation: we partition constraint dependency graphs and use machine learning to predict solver timeouts, guiding per-constraint symbolization decisions. Built on top of KLEE and JFS, our prototype validates the approach on real-world floating-point benchmarks. Results show that selectively symbolizing inputs, guided by predicted solvability and cost, significantly improves coverage efficiency. Our work thus provides both a rigorous theoretical foundation and a practical instantiation for hybrid program analysis.

Symbolic execution faces the challenge of generating valid inputs when analyzing the program with complex input formats. Token-based symbolic execution can partially tackle this challenge but is still doomed by the difficulty of passing input checking and failing to analyze the code after input checking. We propose Lase, an online input grammar synthesis aided symbolic execution method, to generate valid inputs for improving the effectiveness of symbolic execution. Inside Lase, we propose an input grammar-oriented search strategy and a token-level grammar synthesis method. The search strategy selects the paths to cover more syntax rules in priority. The token-level grammar synthesis improves the synthesized grammar's precision and completeness while ensuring efficiency. The experimental results on real-world parsing programs with complex input grammars demonstrate that Lase can improve the coverage of parsing code and generate more valid inputs to improve the coverage of functionality code significantly. Furthermore, compared with the state-of-the-art grammar synthesis methods, the grammars learned by Lase have better precision and recall on most benchmark programs.

Backward-compatible training enables the deployment of advanced models without requiring updates to old gallery databases. However, existing methods, including old-prototype-based (i.e., those relying on prototypes from the old model) and instance-based approaches, often overlook the impact of the old model's quality. High-quality old models exhibit compact intra-class feature distributions, which facilitate effective alignment between old and new models across various methods. In contrast, low-quality old models produce dispersed features, making it difficult for old-prototype-based methods to extract sufficient information. Additionally, instance-based methods are overly restrictive, limiting the flexibility of new models. In this work, we propose SA-BCT, an extremely simple yet effective backward-compatible training method that offers a unified framework for accommodating old models of varying quality. SA-BCT employs a single loss function applied to both old and new features, self-adaptively adjusting the constraint space for new features based on the distribution of old features. Extensive experiments in diverse settings demonstrate the effectiveness of SA-BCT. Code is available at https://github.com/yuleung/SA-BCT.

Hybrid testing that integrates fuzzing, symbolic execution, and sampling has demonstrated superior testing efficiency compared to individual techniques. However, the state-of-the-art (SOTA) hybrid testing tools do not fully exploit the capabilities of symbolic execution and sampling in two key aspects. First, the SOTA hybrid testing tools employ tailored symbolic execution engines that tend to over-prune branches, leading to considerable time wasted waiting for seeds from the fuzzer and missing opportunities to discover crashes. Second, existing methods do not apply sampling to the appropriate branches and therefore cannot utilize the full capability of sampling. To address these two limitations, we propose a novel hybrid testing architecture that combines the precision of conventional symbolic execution with the scalability of tailored symbolic execution engines. Based on this architecture, we propose several principles for combining fuzzing, symbolic execution, and sampling. We implement our method in a hybrid testing tool S$^2$F. To evaluate its effectiveness, we conduct extensive experiments on 15 real-world programs. Experimental results demonstrate that S$^2$F outperforms the SOTA tool, achieving an average improvement of 6.14% in edge coverage and 32.6% in discovered crashes. Notably, our tool uncovers three previously unknown crashes in real-world programs.

With the advancement of satellite computing capabilities, the diversity of satellite communication services imposes varied quality of service (QoS) requirements. Limited satellite resources necessitate remote deployment and updates of running services for QoS testing, increasing testing difficulty. Existing testing tools are limited in functionality or reliant on specific infrastructures, failing to meet the QoS testing needs of edge cloud services in mobile satellite scenarios. In this paper, we present SECTest, an integrated testing platform for QoS in satellite edge clouds. More precisely, SECTest can integrate changes in satellite network topology, create and manage satellite edge cloud cluster testing environments on heterogeneous edge devices, customize experiments for users, support deployment and scaling of various integrated testing tools, provide test data persistence function to manage data life cycle and store data hierarchically, and publish and visualize test results. We have built a real satellite edge cloud cluster based on Kubernetes, integrating both physical and virtual machines, and deploying a variety of integrated testing tools using containerization technology. Currently, we have evaluated the quality of service in terms of processing latency, packet drop rate, throughput, and average response time for object detection microservice applications, web microservice applications, and data transfer tasks. To demonstrate SECTest's scalability in testing network communication protocols, we evaluated the performance of HTTP and gRPC in microservice communication within the cluster. Our experimental results validate SECTest's ability to test key service quality metrics in a real satellite edge cloud cluster.