Guofeng Zhang

Static analysis plays a crucial role in program optimization, bug detection, and automated testing. Dyck-reachability provides a foundational formulation for static analysis, as Dyck grammars can model critical properties such as field and context sensitivity, thus offering broad applicability. This paper shows that static analysis problems modeled as Dyck-reachability on bidirected graphs can be encoded into the EUF SMT theory; consequently, all such problems admit efficient formulation and solution via EUF-based SMT solvers. By leveraging the optimized nature of modern SMT solvers, our method achieves efficiency comparable to state-of-the-art graph-based bidirected Dyck-reachability algorithms while eliminating the need for developing complex specialized graph reachability algorithms. Our approach opens new avenues for solving these classical static analysis problems, demonstrating the strong potential of SMT solvers in encoding static analysis solutions.

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.

High-performance computing (HPC) relies on hardware-specific libraries like BLAS and FFTW, whose correctness is often validated via differential testing. However, manual test cases limit coverage, and automated techniques such as symbolic execution and fuzzing struggle with HPC libraries due to implicit parameter constraints and the difficulty of generating valid, large-scale inputs, leading to inefficiency and poor automation. This paper presents an LLM-powered approach to test driver generation that overcomes these challenges. By classifying interface parameters and modeling their semantic constraints, our method automatically generates executable, structurally valid drivers tailored to HPC libraries. This enables scalable input generation for comprehensive testing of complex APIs. We evaluate our approach on OpenBLAS and FFTW using symbolic execution and fuzzing, showing significant improvements in test automation and coverage compared to manual and baseline automated efforts.

Regression Testing Selection (RTS) reduces the cost of regression testing by only running test cases affected by code changes. Due to the bottleneck of single granularity analyses, the latest RTS techniques tend to analyze with mixed granularities. However, a better synergy of the existing RTS techniques is still challenging. Besides, we have found that once existing RTS approaches use static method-level analysis, handling external library callbacks is difficult, leading to the missed selection of affected test cases. To address these difficulties, we introduce a new hybrid RTS approach, JcgEks, which enhances Ekstazi by integrating static method call graphs. It combines the advantages of dynamic and static analyses, improving precision from class-level to methodlevel and reducing end-to-end time without sacrificing safety. More importantly, JcgEks safely handles external library calls. Besides, we propose a new safety metric and implement the checking tool called Checker to evaluate the safety of RTS tools. We compared JcgEks with four baseline RTS tools in 1000 revisions across 20 open-source projects. The experimental results demonstrate that, compared with the state-of-the-art RTS tool FineEkstazi, JcgEks had the same level of end-to-end testing time and number of selected test classes, while FineEkstazi was confirmed to miss test classes in the experiment. Compared with Ekstazi, JcgEks has reduced end-to-end time by 29% and the number of test classes by 30.9% while ensuring safety.

Regression Test Selection (RTS) minimizes the cost of regression testing by selecting only the tests affected by code changes. We introduce a novel hybrid RTS approach, JcgEks, which enhances Ekstazi by integrating static method call graphs. It combines the advantages of both dynamic and static analyses, improving the precision from class level to method level without sacrificing safety and reducing the overall time. Moreover, it safely addresses the challenge of handling callbacks from external libraries at the static method-level RTS. To evaluate the safety of JcgEks, we insert log statements into code patches and monitor the relationship between the test and the output during execution to gauge the test's impact accurately. The preliminary experimental results are promising.

Serves as an automatic test generation tool designed for C programs based on symbolic execution. employs fuzzing-based pre-analysis and combines static symbolic execution and dynamic symbolic execution to improve the effectiveness of test generation. achieves 5132 scores and is ranked 4th in the branch coverage track of Test-Comp 2024.