Zhendong Su

Ensuring the correctness of mobile payment applications is critical, as even subtle faults can lead to severe financial losses. To ensure reliability, the WeChat Pay (a popular payment app with over one billion active users worldwide) team developed a User Acceptance Testing (UAT) system based on model-based testing (MBT). It maintains use cases specifying user operation sequences and expected app behaviors under business rules. UAT converts these use cases into formal models and generates test cases to validate the app. Although UAT achieves 100% state coverage by covering all user operations and business rules, it still suffers from two major limitations: insufficient test coverage and predefined test oracles. In this paper, we introduce a model-guided property-based testing approach to improving the existing UAT system. We have two key observations: (1) UAT test cases can effectively reach all app states; and (2) WeChat Pay exhibits some invariant behaviors, which can be used to synthesize generic properties for bug finding. Building on these observations, our approach performs random exploration from UAT-discovered states, and validates app behaviors against the automatically synthesized properties. We also propose a greedy trace shrinking algorithm to reduce failure-inducing traces. We implemented our approach as UAT++, an advanced testing tool built upon the UAT system. Across 20,000 machine hours, UAT++ found 59 previously unknown bugs, including 48 logic bugs and 11 crash bugs (55 confirmed, 45 fixed). These bugs could not be found by the UAT system and classic property-base testing (PBT). UAT++ improved state transition coverage by 82.6% and 600.0% over the UAT system and classic PBT, respectively. The shrinking algorithm attained an average trace reduction rate of 79.9%. To date, UAT++ has been deployed in the continuous testing pipeline of WeChat Pay across Android, iOS, and HarmonyOS platforms.

Property-based testing (PBT) is a popular software testing methodology and is effective in validating the functionality of mobile applications (apps for short). However, its adoption in practice remains limited, largely due to the manual effort and technical expertise required to specify executable properties. In this experience paper, we propose a novel structured property synthesis approach that automatically translates property descriptions in natural language into executable properties, and implement it in a tool named iPBT. Our approach decomposes the problem into UI semantic grounding and executable property synthesis. It first builds an enriched widget context via multimodal LLMs to align visual elements with their functional semantics, and then uses an LLM with in-context learning to generate framework-specific executable properties. We evaluate with a closed-source LLM (GPT-4o) and an open-source LLM (DeepSeek-V3) on 160 diverse property descriptions across 20 apps (124 from an existing benchmark and 36 newly authored). iPBT achieves 95.0% (152/160) accuracy on both LLMs. Notably, an ablation study reveals that the enriched widget context contributes to an absolute improvement of up to 18.1% (from 76.9% to 95.0%). A user study with 10 participants demonstrates that iPBT reduces the time required to write executable properties by 56%, suggesting substantially lower manual effort. Furthermore, evaluations on 1,520 linguistically diverse paraphrases of the original property descriptions further confirm iPBT’s robustness, achieving 88.2% accuracy on GPT-4o and 87.8% on DeepSeek-V3.

Computation pushdown is a critical technique in distributed database management systems (DBMSs), enabling certain operations to be executed closer to the data to reduce network overhead and improve performance. However, its behavior depends on multiple factors beyond the input query itself, such as data distribution and resource utilization. This makes it difficult to validate correctness using only input queries in a black-box manner. Existing testing methods that rely solely on query manipulation cannot effectively control or predict pushdown behavior, and are therefore insufficient. In this paper, we introduce Controlled Pushdown Execution (CPE), a white-box method that enables systematic validation of computation pushdown. CPE modifies the source code of DBMSs to forbid a specific pushdown operator and compares the results. Any discrepancy reveals a bug. Our study shows that CPE can control all supported operators across different systems. We applied CPE to three production-grade distributed DBMSs: CockroachDB, TiDB, and YugabyteDB. CPE found 25 previously unknown and unique bugs, 14 of which are logic bugs---incorrect results. CPE finds 3x more bugs than historical bugs and can reproduce all historical bugs. Beyond computation pushdown, the core insight of controllable execution can generalize to other contexts (e.g., transaction schedule), providing a systematic way to uncover subtle logic bugs.

Path coverage tracing is one of the fundamental components for supporting a wide range of dynamic program analyses, such as testing, debugging, profiling, and many others. Since one needs to insert code into a program to trace its coverage, runtime overhead becomes the main bottleneck for scalability. As finding the minimum number of instrumentation points is NP-hard, extensive work has focused on reducing the number of instrumented edges under diverse assumptions, and thus suffers from the trade-off between precision and efficiency. Departing from this edge-centric view, we introduce, in this work, a novel perspective, namely the node-centric view, where we aim to find the minimum number of blocks, rather than edges as in existing work, that can differentiate all edges and paths in the program. This new perspective allows us to design a linear-time algorithm that is provably correct and optimal—it finds the minimum set of blocks for correctly differentiating edge/path coverage for arbitrary control-flow graphs. Our key insight is that optimal node-level instrumentation only needs to distinguish undifferentiated paths at the block where they converge, enabling our algorithm to have linear-time complexity regarding the number of basic blocks. We implement our algorithm as InsOpt and compare it against state-of-the-art edge-coverage instru- mentation techniques on the real-world vulnerability-detection benchmark, Magma. Our evaluation results demonstrate significant improvements: InsOpt needs 2.8x less instrumentation with only 17% basic blocks instrumented. This reduced instrumentation yields a 1.6x speedup and a substantial 2.4x reduction in runtime overhead. Moreover, we also demonstrate substantial potential for InsOpt across other applications. Specifically, our integration of InsOpt with AFL++, a state-of-the-art fuzzer, shows a 5.0x speedup in vulnerability detection and a 1.5x performance improvement. Notably, this efficiency gain further benefits InsOpt in detecting five previously unknown bugs in frequently evaluated projects by other state-of-the-art tools.

Background. Large language models are increasingly deployed as tutors in introductory programming courses, yet evidence that they actually improve learning remains thin, and their tendency to shortcut productive struggle raises concerns about pedagogical harm. Self-regulated learning (SRL) and cognitive engagement (CE) frameworks offer a principled way to address this, but whether embedding them in system prompts actually changes how students learn is an open question. Objectives. We investigated whether AI tutors guided by SRL and CE frameworks affect conceptual understanding, perceived usability, cognitive load, student engagement, and other outcomes when compared to a pedagogically constrained baseline tutor in CS1. Methods. We conducted a preregistered, three-armed crossover study over six weeks of authentic coursework, comparing a baseline AI tutor against two SRL and CE-guided tutors designed to model Zimmerman’s cyclical model, which scaffolds planning, monitoring, and reflection, and Chi’s ICAP framework, which promotes progressively deeper forms of cognitive engagement. We assessed outcomes using post-exercise surveys, conceptual multiple-choice questions, in-platform ratings, and coded responses from the interaction logs, and analyzed the quantitative measures with mixed-effects models. Findings. On the four preregistered confirmatory measures, we found no statistically significant differences between conditions. Non-confirmatory analysis showed that students spent significantly more time on task, wrote longer messages, and produced more constructive contributions when interacting with SRL and CE tutors. Furthermore, the relationship between cognitive load and quiz performance differed significantly by agent type. Implications. Our results suggest that the pedagogical behavior of AI tutors may not be easily steered through system prompts alone: embedding established SRL and CE frameworks did not produce detectable improvements on any preregistered outcome in a large, ecologically valid deployment. Rather than prescribing a single tutoring strategy, future designs may benefit from giving students greater agency over the kind of help they receive, allowing them to choose between scaffolded and more direct support based on their own needs.

Modern infrastructures rely on Infrastructure as Code (IaC) systems to keep complex deployments consistent, reproducible, and scalable at production scale. The reliability of these infrastructures, however, depends on the correctness of their building blocks, which are reusable components (modules) that each performs a dedicated task, such as installing a package, managing an OS user, or configuring a service, and reconciling its state with the desired specification. A central promise of these components is portability: a specification written once should correctly manage the targeted resource on every OS the IaC component supports. When this property is violated, defects can propagate across entire infrastructures, causing outages, security vulnerabilities, and costly misconfigurations. In this work, we introduce crOSsible, the first automated framework for cross-OS testing of IaC modules. crOSsible leverages large language models (LLMs) to synthesize and repair integration tests from structured module documentation, and executes them across 13 versions of 8 major Linux distributions. While our techniques are generally applicable to different IaC systems, we instantiate and evaluate them on Ansible, the most widely used IaC framework for managing individual servers. Evaluation across 259 popular Ansible modules demonstrates both effectiveness and real-world impact. In just 12 hours of testing, crOSsible uncovered 36 previously unknown bugs, including 22 portability violations. In total, 27 issues have been confirmed by maintainers, with 17 already fixed. The discovered issues range from crashes to dangerous soundness defects where modules reported success despite leaving systems misconfigured. Beyond bug discovery, crOSsible improved the code coverage of Ansible modules by 12.3% on average, systematically exercising OS-specific code paths that existing tests missed.