arXiv CSopen access

From Exploration to Specification: LLM-Based Property Generation for Mobile App Testing

From Exploration to Specification: LLM-Based Property Generation for Mobile App Testing Yiheng Xiong

Singapore Management University Singapore [email protected]

Shiwen Song

Singapore Management University Singapore [email protected]

arXiv:2604.13463v1 [cs.SE] 15 Apr 2026

Ting Su

East China Normal University China [email protected]

Abstract Mobile apps often suffer from functional bugs that do not cause crashes but instead manifest as incorrect behaviors under specific user interactions. Such bugs are difficult to detect by conventional automatic testing techniques because they often lack explicit test oracles. Property-based testing can effectively expose them by specifying intended behavior as properties and checking them under diverse interactions. However, its practical use is limited by the need for manually written properties, which are difficult and expensive to construct. To address this limitation, this paper explores the use of large language models (LLMs) to automate property construction for property-based testing of mobile apps. This process is challenging in two ways. First, it is difficult to systematically uncover and execute diverse app functionalities. Second, it is difficult to derive valid properties from functionality execution results, because a single execution provides only limited evidence about what behavior should generally hold. To address these challenges, we introduce PropGen, which performs functionality-guided exploration to collect behavioral evidence from execution results, synthesizes properties from the collected evidence, and refines imprecise properties based on testing feedback. We implemented PropGen and evaluated it on 12 real-world Android apps. The results show that PropGen can effectively identify and execute app functionalities, generate valid properties, and refine most imprecise ones. Across all apps, PropGen identified 1,210 valid functionalities and correctly executed 977 of them, compared with 491 and 187 for the baseline. It generated 985 properties, 912 of which were valid, and successfully refined 118 of 127 imprecise ones exposed during testing. Using the resulting properties, we found 25 previously unknown functional bugs in these apps, many of which were missed by existing testing techniques.

1

Introduction

Mobile apps are highly interactive and stateful systems whose functionalities are largely driven by user interface interactions. Despite extensive testing efforts, functional bugs (e.g., incorrect interaction logic) remain prevalent in real-world apps [67]. These bugs often do not manifest as crashes, making them difficult to detect using conventional GUI testing techniques that mainly emphasize code coverage or crash discovery [8, 17, 29, 31, 33, 38, 47, 58, 61]. Manual testing (e.g., writing GUI tests) is widely used in practice to validate

Bo Ma

East China Normal University China [email protected]

Xiaofei Xie

Singapore Management University Singapore [email protected] the functional correctness of mobile apps [24, 26]. However, it is brittle, costly to maintain, and typically covers only pre-defined happy paths, often missing non-trivial functional bugs [66]. Property-based testing (PBT) offers a promising direction for addressing this challenge [5]. Recent work has demonstrated that carefully designed properties can reveal non-trivial functional bugs that are missed by other techniques [52, 66]. In mobile app testing, developers specify expected behaviors as properties, and a PBT framework then automatically generates a large number of GUI events to explore diverse GUI states and check whether these properties hold. Compared with validating only a fixed set of manually crafted GUI test cases, this paradigm provides a more efficient way to assess functional correctness across diverse GUI states. However, the effectiveness of PBT fundamentally depends on the availability of high-quality properties, whose manual construction remains a major barrier to practical adoption [15, 16]. This challenge is especially pronounced for mobile apps, where explicit behavioral specifications are often unavailable. As a result, testers must manually understand app functionalities, abstract their expected behaviors into executable properties, and refine the properties when reported violations are false positives. This manual and iterative process substantially limits the broader adoption of PBT. To address this limitation, a promising direction is to leverage the reasoning and code-generation capabilities of Large Language Models (LLMs) to automate property construction. However, directly asking an LLM to generate properties is often unreliable, due to both the lack of explicit behavioral specifications in mobile apps and the tendency of LLMs to hallucinate. Instead, an effective solution should be able to identify app functionalities, infer properties from execution-derived behavioral evidence, and refine imprecise properties based on testing feedback. Challenges. However, achieving this goal is far from straightforward and presents two key challenges: broad functionality exploration and property abstraction from execution traces. First, the approach must explore as many meaningful app functionalities as possible, but this is difficult in mobile apps. Many functionalities are not directly visible on the current screen. They may only become available after several navigation steps, under specific UI states, or through transient interface elements such as menus and dialogs. As a result, systematically exposing a large and diverse set of functionalities through app exploration is non-trivial. Without sufficient functionality exposure, the generated properties can cover only

Conference’17, July 2017, Washington, DC, USA

a limited portion of app behavior. Second, even after a functionality is executed, it is still difficult to infer a valid property from the execution traces. This is because a property must capture the essential behavior of the functionality, rather than merely describe one observed execution. In practice, however, the execution trace (e.g., events and screenshots) is often noisy and low-level, and only provides a single concrete behavioral instance. Moreover, the inferred property can become inaccurate: it may encode details that happen to hold in the current trace, but do not necessarily hold in other valid contexts. Such imprecision can lead to false positives during testing and reduce the usefulness of the generated properties. Importantly, this difficulty is also faced by human developers when manually writing properties. Our approach. To address the first challenge, we design a functionality hypothesis-guided exploration strategy that systematically uncovers executable app functionalities and collects behavioral evidence from their executions. Given a GUI state, our approach infers candidate functionalities and grounds each of them in concrete actionable widgets, making the inferred functionality hypothesis both reliable and directly executable. Based on these hypotheses, our approach performs targeted functionality execution. During this process, it incrementally expands the functionality pool when new functionality appears, reuses previously inferred functionalities across recurrent GUI states, and falls back to lightweight random exploration only when no functionality is available. This hybrid strategy improves functionality coverage and enables richer behavioral evidence collection under a limited exploration budget. To address the second challenge, PropGen adopts property generation from behavior evidence followed by feedback-driven refinement. Instead of generating properties directly from execution results, PropGen first abstracts each functionality execution trace into a compact condition–action–outcome representation, derives a structured property description, and then translates it into the executable property. Because properties inferred from limited evidence may still over-generalize, PropGen further refines those that trigger false positives during testing. Each refinement is anchored to the behavioral evidence, allowing PropGen to localize whether the issue lies in the precondition, interaction, or postcondition and apply a targeted refinement. Through this process, PropGen improves property precision and robustness while preserving the original intent. Evaluation and results. We implemented our approach as a tool named PropGen and evaluated it on 12 real-world popular and diverse Android apps. Across all apps, PropGen inferred 1,282 functionalities, of which 1,210 (94.4%) were valid and 977 (76.2%) were correctly executed. In comparison, the baseline approach inferred 575 functionalities, with 491 valid and 187 correctly executed. It further generated 985 property descriptions, 912 (92.6%) of which were valid. During property-based testing, 127 properties were found to be imprecise, and 118 (93.7%) of them were successfully refined by our refinement technique. Using the generated properties, we found 25 previously unknown functional bugs in the latest versions of the subject apps, whereas existing functional testing techniques could find only 3 of them in practice. These results demonstrate the effectiveness of our approach in automating property construction for mobile apps, as well as the bug-finding capability of the resulting properties.

Yiheng Xiong, Shiwen Song, Bo Ma, Ting Su, and Xiaofei Xie

In summary, this paper makes the following contributions: • We propose a novel approach that automatically explores app functionalities and generates properties from runtime behavioral evidence, without relying on manual specifications. • We design a hypothesis-driven behavioral evidence construction technique that infers functionalities from GUI states and summarizes execution traces into structured representations suitable for property synthesis. • We develop a property synthesis and refinement approach that derives properties from behavior evidence and refines imprecise properties through execution feedback. • We implement our approach as PropGen and conduct an extensive evaluation on 12 real-world Android apps. The results show that PropGen can cover a large number of app functionalities while achieving high functionality and property validity, and can effectively refine most imprecise properties.

2

Background

Property-based testing. Property-based testing is a powerful testing methodology that validates whether a program satisfies general properties rather than specific input-output examples [5]. Instead of writing example-based test cases, testers specify high-level properties that describe the expected behavior of the system. Then, a PBT framework automatically generates a large number of test inputs and executes them to verify whether the properties hold. For example, for a sorting function sort, rather than enumerating concrete examples (e.g., sort([3,1,2])== [1,2,3]), one can define a general property such as idempotence: sort(sort(x)) = sort(x). The PBT framework then generates a large number of inputs to verify this property and reports any violating input as a counterexample. GUI state, event, and functionality. Android applications are GUI-driven and event-based. When an app A runs, its runtime state is represented by its current GUI layout, which we denote as a GUI state 𝑠. A GUI state corresponds to a hierarchical tree ℓ, whose nodes are GUI widgets 𝑤 (e.g., Button, TextView, EditText) with attributes (e.g., text, resourceId) and interaction capabilities. User interactions are modeled as events. An event is defined as 𝑒 = ⟨𝑡, 𝑤, 𝑑⟩, where 𝑡 is the event type (e.g., click), 𝑤 is the target widget, and 𝑑 is optional data (e.g., text input). An app execution is modeled as a sequence of events. Given 𝐸 = [𝑒 1, . . . , 𝑒𝑛 ], executing 𝑒1

𝑒𝑛

A produces a trace 𝜏 = 𝑠 0 −→ 𝑠 1 → − · · · −−→ 𝑠𝑛 , or 𝑠 0 ⇝ 𝑠𝑛 , where 𝑠 0 is the initial state. Then, we define a functionality as a tuple 𝑓 = ⟨𝑑, 𝜏⟩, where 𝑑 is a semantic intent of a functionality (e.g., "create a note"), and 𝜏 is an execution trace that realizes this functionality. 𝐸

Concretely, 𝜏 has the form 𝑠 ⇝ 𝑠 ′ , where 𝐸 is a sequence of one or more events executable from GUI state 𝑠. Executing 𝜏 completes the corresponding functionality and produces a concrete effect on the app state. Property-based testing for mobile apps. In property-based testing for mobile apps, a property specifies an expected behavior of the app. A property can be defined as a tuple 𝜙 = ⟨𝑃, 𝐼, 𝑄⟩, where 𝑃 specifies the GUI states where the property applies, 𝐼 is the interaction scenario, and 𝑄 specifies the expected outcome after executing 𝐼 . During testing, when a GUI state 𝑠 satisfies 𝑃, the interaction scenario 𝐼 is executed from 𝑠 to reach a new state 𝑠 ′ . The property 𝐸

From Exploration to Specification: LLM-Based Property Generation for Mobile App Testing

is satisfied when (𝑠 |= 𝑃 ∧𝑠 ⇝ 𝑠 ′ ) ⇒ 𝑠 ′ |= 𝑄; Otherwise, a property violation is reported. 𝐼

3

Approach

Overview. Given an app, PropGen automatically generates properties from runtime executions and further refines imprecise ones based on testing feedback. Figure 1 presents the overall workflow, which consists of three stages. First (§3.1), PropGen performs hypothesis-driven dynamic exploration to construct behavioral evidence. For each encountered GUI state 𝑠, it infers functionality hypothesis grounded in the visible UI widgets, executes selected functionalities, and summarizes the resulting execution traces into behavioral evidence for downstream property generation. Second (§3.2), PropGen synthesizes properties directly from the behavioral evidence constructed in the first stage. Specifically, it first generates natural-language property descriptions that capture the intended condition–event–outcome relation, and then translates them into executable properties. Third (§3.3), PropGen validates the generated properties by the PBT framework and refines properties that are found to be improperly specified. Illustrative example. Figure 2 illustrates the workflow of PropGen on a note-taking app. Starting from the first page in Figure 2 (a), PropGen performs behavioral evidence construction by inferring multiple candidate functionality hypotheses from the current GUI state. It then selects one hypothesis, attaching a photo to the note, and executes the corresponding interaction sequence, i.e., opening the attachment menu, choosing Camera, taking a photo, and returning to the note page. The execution trace is summarized into structured behavioral evidence (as shown in Figure 2(c)), from which PropGen synthesizes an executable property describing the expected behavior of this functionality (Figure 2(d)). The initial synthesized property may be imprecise and thus produce false positives during execution. In this example, its postcondition checks whether the app returns to a page containing the text “Notes” and whether the newly added attachment is displayed as an attachment thumbnail. This postcondition is too specific. After taking a photo, the app may legitimately return to either the Notes page or the Archive page, depending on where the note was opened. Moreover, under reduced view, the attached photo may not appear as a thumbnail, but instead as a compact attachment icon (Figure 2(b)). Therefore, the synthesized property may incorrectly flag a failure even though the photo has been successfully attached. PropGen then refines the property by relaxing these assertions to allow multiple valid return pages (use the menu button that both pages contain) and attachment representations (thumbnail or icon). After validating this property using the PBT tool Kea, we uncovered a new functional bug: opening audio recording before taking a photo prevents the photo attachment from appearing.

3.1

Behavioral Evidence Construction

The goal of this stage is to construct execution-grounded behavioral evidence for downstream property synthesis. Instead of relying on external specifications, PropGen systematically explores executable app functionalities and records their runtime interaction traces as behavioral evidence. Algorithm 1 summarizes the workflow.

Conference’17, July 2017, Washington, DC, USA

Algorithm 1 Behavioral Evidence Construction Require: Target app A, time budget 𝐵 Ensure: Behavioral evidence set T̂ 1: Launch A; obtain initial state 𝑠 2: G𝐹 ← ∅, U ← ∅, T̂ ← ∅ 3: while elapsed time < 𝐵 do 4: 𝑢 (𝑠) ← Extract(𝑠) ⊲ Extract the widgets 5: if UnseenWidgets(𝑢 (𝑠), U) then 6: 𝐹 (𝑠) ← Inferhypothesis(𝑠) ⊲ infer the hypothesis 7: G𝐹 ← G𝐹 ∪ 𝐹 (𝑠) ⊲ add the hypothesis into global pool 8: U ← U ∪ 𝑢 (𝑠) 9: end if 10: if HasUnexplored(G𝐹 (𝑢 (𝑠))) then 11: 𝑓 ← Select(G𝐹 (𝑢 (𝑠))) 12: (𝜏 𝑓 , 𝑠 ′, G𝐹 , U) ← Execute(𝑓 , 𝑠, G𝐹 , U) 13: T̂ ← T̂ ∪ {Summarize(𝜏 𝑓 )} ⊲ evidence summary 14: MarkExplored(𝑓 , G𝐹 ) 15: 𝑠 ← 𝑠′ 16: else 17: 𝑠 ← RandomExplore(𝑠) 18: end if 19: end while 20: return T̂

Given a target app A and a time budget 𝐵, PropGen first launches the app and initializes the global functionality pool G𝐹 , the set of observed UI contexts U, and the behavioral evidence set T̂ (Lines 1– 2). It then iteratively explores the app until the budget is exhausted (Lines 3–19). In each iteration, PropGen extracts the current GUI context from the current GUI state (Line 4). If the context contains previously unseen widget evidence, PropGen invokes a Multimodal Large Language Model (MLLM) to infer functionality hypotheses for the current state, adds them to G𝐹 , and updates U (Lines 5–8). PropGen then checks whether the current context contains any unexplored functionality hypothesis (Line 10). If so, it selects one hypothesis together with its triggering widget, executes it to obtain a functionality trace, and summarizes the trace into a behavioral evidence item added to T̂ (Lines 11–15). Otherwise, PropGen performs lightweight random exploration to leave the current local GUI region and expose new interaction opportunities (Lines 16– 17). The process repeats until the time budget is exhausted, after which PropGen returns the collected behavioral evidence set T̂ (Lines 19–20). 3.1.1 Functionality Hypothesis Generation. Given a GUI state 𝑠 encountered during exploration, this step aims to infer which app functionalities may be executable under the current interface context. To support subsequent execution, each inferred functionality is associated with a concrete triggering widget in the current state. Semantic context construction. To support functionality inference, PropGen first constructs a semantic context for the current GUI state 𝑠. This context includes three parts: the screen-level context of the current state, app-level semantic cues, and cross-state functionality memory. The screen-level context is derived from the current GUI screenshot, where each interactive widget 𝑤 in 𝑠

Conference’17, July 2017, Washington, DC, USA

Yiheng Xiong, Shiwen Song, Bo Ma, Ting Su, and Xiaofei Xie

Property Synthesis from Behaviroal Evidence

Behavioral Evidence Construction

Property Description Generation

Semantic Context Construction

Functionality selection

Hypothesis Inference

Event Planing and Execution

Executable Property Translation

Feedback-Driven Property Refinement Executable Property

Output

Validation by PBT tool

Property Description

Failed Infomation App Under Test

Behavioral Evidence Summarization

Functionality Hypothesis

Property Refinement

Imprecise Property Failure Evidence

Executable Property

Figure 1: Overview of PropGen.

① Behavior Evidence Construction

(a) An execution trace of the functionality.

② Property Synthesis

(c) Behavior evidence.

(b) Suspicious violation.

③ Feedback-Driven Property Refinement (d) Generated property.

Figure 2: An Illustrative Example of Behavioral Evidence Construction, Property Synthesis, and Feedback-Driven Property Refinement for a Note-Taking App. is annotated with a unique numeric label. These labels turn visually distributed UI elements into explicit references, allowing the inferred functionalities to be grounded in concrete widgets. The app-level semantic cues include the app name and the list of activity names extracted from the AndroidManifest.xml file, helping the MLLM interpret the current screen under the broader semantic context of A. Finally, the cross-state functionality memory stores previously inferred functionalities, helping avoid repeatedly rediscovering semantically similar functionalities in later GUI states. Together, these components provide the contextual information needed for inferring plausible user-facing functionalities from 𝑠. Functionality hypothesis inference. Using the constructed semantic context, PropGen invokes a MLLM to infer candidate functionality hypothesis for the current GUI state 𝑠. Formally, the inferred hypothesis are represented as 𝐹 (𝑠) = [⟨𝑓1, 𝑤 1 ⟩, ⟨𝑓2, 𝑤 2 ⟩, . . . ,

⟨𝑓𝑘 , 𝑤𝑘 ⟩], where each functionality hypothesis 𝑓𝑖 is a concise naturallanguage description of a candidate app functionality, and 𝑤𝑖 denotes its corresponding triggering widget. This widget grounding serves two purposes. First, it constrains the MLLM to infer functionalities that are supported by the current GUI state, reducing unsupported or non-actionable predictions. Second, it makes the inferred functionalities directly executable in subsequent exploration. The inferred functionality hypothesis, together with their associated triggering widgets, are then stored in the global functionality pool G𝐹 to support later execution and cross-state reuse. Inference triggering and hypothesis reuse. To avoid redundant MLLM invocations on similar GUI states, PropGen triggers functionality inference only when a newly visited state introduces unseen widget evidence. It maintains a global set of explored UI contexts U = {𝑢 1, 𝑢 2, . . .}, where each context is defined as 𝑢 (𝑠) =

From Exploration to Specification: LLM-Based Property Generation for Mobile App Testing

⟨𝑎(𝑠),𝑊 (𝑠)⟩, with 𝑎(𝑠) denoting the activity and 𝑊 (𝑠) the set of signatures of leaf-level interactive widgets. For each state 𝑠, PropGen compares 𝑊 (𝑠) with existing contexts under the same activity. If no new widget signatures are observed, it reuses previously inferred functionality hypotheses; otherwise, it invokes the MLLM to infer new functionalities and updates the global pool G𝐹 . To enable stable comparison across screens, each widget 𝑤 is represented by a signature of attributes ⟨𝑐𝑙𝑎𝑠𝑠, 𝑟𝑒𝑠𝑜𝑢𝑟𝑐𝑒𝐼𝑑, 𝑡𝑒𝑥𝑡, 𝑑𝑒𝑠𝑐𝑟𝑖𝑝𝑡𝑖𝑜𝑛⟩, which are commonly used to identify unique widgets in practice [47, 49, 64]. To reduce noise from dynamic content, PropGen retains only app-defined text in signatures by filtering widget text against a whitelist extracted via static analysis. This avoids treating semantically identical screens with transient text differences as distinct contexts. 3.1.2 Hypothesis-Guided Functionality Execution. Given the global functionality pool G𝐹 generated in § 3.1.1, the goal of this step is to expand behavioral coverage under a limited exploration budget by executing app functionalities in a targeted manner. Instead of interacting with A through arbitrary GUI events, PropGen treats each functionality hypothesis in G𝐹 , together with its associated triggering widget, as an explicit execution target, and prioritizes the execution of previously unexplored functionality hypothesis. Executing a selected functionality hypothesis ⟨𝑓 , 𝑤⟩ may require one or more concrete GUI events, thereby inducing state transitions 𝐸

of the form 𝑠 → − 𝑠 ′ . Such functionality-guided execution serves two purposes simultaneously: it exercises already identified app behaviors to collect behavioral evidence, and it drives the app into new GUI states 𝑠 ′ from which additional functionality hypothesis 𝐹 (𝑠 ′ ) can be inferred and inserted into G𝐹 . In this way, execution and hypothesis generation form a closed exploration loop that progressively broadens the functionality space explored by PropGen. Functionality selection. At each GUI state 𝑠, PropGen retrieves from G𝐹 the candidate functionality hypothesis associated with the current UI context 𝑢 (𝑠), denoted as G𝐹 (𝑢 (𝑠)). Since the exploration budget is limited, PropGen does not execute these candidates arbitrarily, but prioritizes those with higher expected exploration utility. This prioritization is implemented using lightweight heuristics guided by three considerations: whether the functionality corresponds to a main app behavior, whether it is semantically different from previously executed functionalities, and whether it is likely to be successfully executed in the current context. Based on these heuristics, the top-ranked unexplored functionality hypothesis ⟨𝑓 , 𝑤⟩ is selected as the next execution target. The selected hypothesis is then passed to a goal-directed interaction loop that incrementally plans, executes, and evaluates UI actions until the functionality is completed or a step limit is reached. Event planning and execution. Once a functionality hypothesis ⟨𝑓 , 𝑤⟩ is selected, PropGen executes it through a goal-directed interaction loop consisting of event planning, guarded execution, and post-event evaluation. At each step 𝑖, PropGen first predicts the next GUI event based on three sources of information: the functionality goal 𝑓 , the execution history 𝐻𝑖 of prior events and their outcomes, and the current GUI state 𝑠𝑖 , represented as a screenshot with labeled widgets. The predicted event is denoted as 𝑒𝑖 = ⟨𝑡𝑖 , 𝑤𝑖 , 𝑑𝑖 ⟩, where the event type 𝑡𝑖 is chosen from a predefined event space including click, long-click, edit, swipe, and back, the target

Conference’17, July 2017, Washington, DC, USA

widget 𝑤𝑖 is specified by its numeric label, and 𝑑𝑖 ) specifies the attached data (e.g., input text). Before executing 𝑒𝑖 , PropGen verifies that the referenced widget 𝑤𝑖 is present in the current state 𝑠𝑖 . If the predicted widget identifier is invalid, the event is skipped and directly labeled as a failed step. This guarded execution mechanism prevents invalid model-predicted interactions and improves execution robustness. 𝑒𝑖 After execution produces a state transition 𝑠𝑖 −→ 𝑠𝑖+1 , PropGen evaluates whether the step has advanced the selected functionality. This evaluation jointly considers the pre- and post-event GUI states, the functionality hypothesis 𝑓 , and the accumulated execution history 𝐻𝑖 . Based on this evidence, the MLLM assigns an outcome label 𝑜𝑖 ∈ {success, fail, complete} to the current step. Here, success indicates meaningful progress toward the functionality goal, fail indicates that the event was unproductive for the intended functionality, and complete indicates that the functionality goal has been achieved. The resulting step and outcome are then incorporated into the execution history for subsequent planning, while complete terminates execution of the current functionality. Behavioral evidence summarization. To support downstream property synthesis, PropGen summarizes each executed interaction trace into compact behavioral evidence. This step is necessary because raw execution traces are low-level, noisy, and specific to a single execution, whereas property synthesis requires a higher-level representation of the condition–event–outcome relation exhibited by the app behavior. To bridge this gap, PropGen incrementally 𝑒𝑖 converts each interaction step 𝑠𝑖 −→ 𝑠𝑖+1 into a structured transition with five elements: the state summary before the event, an event summary describing the interaction performed, the state summary after the event, a state-diff summary capturing the visible difference between the two GUI states, and an outcome label 𝑜𝑖 indicating how the event affected progress toward the selected functionality. The state summaries are functionality-oriented: they describe the screen context, visible actionable elements, current content state, and observable feedback cues. In contrast, the state-diff summary focuses on the concrete GUI changes induced by the interaction. Together, these summaries preserve the behavioral evidence needed to capture the executed functionality’s condition–event–outcome relation while filtering out incidental GUI details. The resulting summarized trace, denoted as 𝜏ˆ𝑓 , serves as the behavioral evidence used in the subsequent property synthesis stage. Exploration beyond local hypothesis exhaustion. As exploration proceeds, PropGen may reach GUI states where all available functionality hypothesis have already been executed and no new hypothesis can be triggered. In such cases, continued MLLM-guided exploration becomes less effective, because the MLLM is most useful when acting toward an explicit functionality goal. When no such goal is available, the task is no longer to reason about how to execute a functionality, but simply to move the app into a new GUI region where new functionality hypothesis may emerge. For this purpose, lightweight random exploration is both more efficient and less costly. Therefore, once local functionality-guided exploration is exhausted, PropGen switches to random exploration. It continues traversing the app through random GUI events until it reaches a state that either contains unexecuted functionality hypothesis or exposes unseen widget evidence for new hypothesis generation.

Conference’17, July 2017, Washington, DC, USA

In the former case, PropGen resumes functionality-guided execution directly; in the latter, it first performs functionality hypothesis generation and then continues execution. This design combines the strength of goal-directed MLLM-guided execution with the efficiency of random exploration for escaping locally exhausted GUI regions.

3.2

Property Synthesis from Behavior Evidence

The goal of this stage is to derive executable properties from the behavioral evidence collected during functionality exploration. As input, PropGen takes the summarized trace 𝜏ˆ𝑓 produced in Section 3.1, which compactly captures how a functionality is exercised and what observable GUI outcome it induces. Each synthesized property takes the form 𝜙 = ⟨𝑃, 𝐼, 𝑄⟩, where 𝑃 is a precondition, 𝐼 is an interaction scenario, and 𝑄 is a postcondition assertion. Rather than generating 𝜙 directly from 𝜏ˆ𝑓 , PropGen decomposes property synthesis into two steps, separating semantic property formulation from executable code generation. It first constructs a natural-language property specification that explicitly captures the intended ⟨𝑃, 𝐼, 𝑄⟩ relation, and then translates this intermediate specification into executable property code. Natural-language property description generation. Based on the summarized trace 𝜏ˆ𝑓 , PropGen first prompts the MLLM to construct a natural-language property specification 𝜙 𝑁 𝐿 = ⟨𝑃, 𝐼, 𝑄⟩ for the functionality captured by the behavioral evidence. The summarized trace provides structured evidence about the execution context, performed interactions, observable state changes, and step outcomes. Rather than merely restating these observations, the MLLM is guided to abstract from 𝜏ˆ𝑓 a generalized behavioral rule that should hold across executions of the same functionality. The inferred specification 𝜙 𝑁 𝐿 consists of three parts: a precondition 𝑃 describing the observable GUI context in which the property should be checked, an interaction scenario 𝐼 capturing the user events needed to exercise the functionality, and a postcondition 𝑄 specifying the immediate visible effect that should hold afterward. To improve precision and executability, PropGen constrains this inference process in three ways. First, 𝑃 must be grounded in observable UI evidence and sufficiently specific to avoid triggering the property on unrelated screens with superficially similar widgets. Second, 𝑄 must focus on effects that are directly and reliably verifiable from the GUI, such as the appearance, disappearance, or modification of visible widgets or content. Third, the inferred specification should avoid trace-specific brittle details, such as incidental text instances or unstable widget states, and instead capture functionality semantics in a form that remains robust across executions. In this way, PropGen lifts concrete execution evidence into a generalized, testable property abstraction. The resulting naturallanguage specification makes the intended property semantics explicit before code generation, thereby separating behavioral understanding from executable realization. Executable property translation. Given the inferred naturallanguage property specification 𝜙 𝑁 𝐿 = ⟨𝑃, 𝐼, 𝑄⟩, PropGen translates it into executable property code for the target PBT framework. Specifically, this step realizes the precondition 𝑃, interaction scenario 𝐼 , and postcondition 𝑄 using the framework’s property structure and API conventions, thereby producing a runnable property implementation. Since the intended property semantics have

Yiheng Xiong, Shiwen Song, Bo Ma, Ting Su, and Xiaofei Xie

already been made explicit in the preceding natural-language formulation step, this translation primarily serves to operationalize the structured specification rather than to perform further behavioral inference. This step is implemented by prompting the LLM with the generated natural-language specification together with frameworkspecific APIs and widget attributes, with reference to the prompt design in prior work on translating natural-language properties into executable ones [65]. The resulting code is then passed to the subsequent validation and refinement stage.

3.3

Feedback-Driven Property Refinement

Properties automatically generated from functionality traces may still be imprecise and therefore trigger false positives during testing. However, a reported failure should not be refined by simply adapting the property to that single execution, because such a fix may overfit the observed case and drift away from the original functionality intent. Our key idea is that refining a false-positive-inducing property requires first recovering the property’s original testing intent, and then revising it so that it remains valid for both the original intended execution and the newly observed legitimate execution. To this end, we ground refinement in the source summarized trace from which the property was originally inferred, rather than treating refinement as unconstrained rewriting. Specifically, PropGen reasons about the refinement using both the source summarized trace and the failure-triggering execution. Specifically, it first recovers the original testing intent of the property by locating the relevant segment in 𝜏ˆ𝑓 that matches the property’s triggering context, interaction scenario, and expected outcome. It then compares this trace-grounded intended behavior with the failing execution to explain why the violation occurs and identify which component of 𝜙 has become imprecise, i.e., the precondition 𝑃, the interaction scenario 𝐼 , or the postcondition 𝑄. Based on this diagnosis, PropGen refines only the faulty component through a minimal modification. More specifically, it strengthens 𝑃 when additional UI guards are needed, revises 𝐼 when the event sequence does not faithfully reflect the intended behavior, and relaxes or simplifies 𝑄 when the assertion is overly specific. In this way, the refined property remains consistent with both the sourcetrace execution and the newly observed legitimate execution, while preserving the original testing intent as much as possible.

4

Implementation

We implemented PropGen as an end-to-end prototype for automated property generation on Android apps. The system is primarily written in Python and JavaScript, and integrates three key capabilities: GUI state acquisition and interaction, multimodal LLMbased reasoning, and executable property generation for Kea [66]. At runtime, PropGen uses uiautomator2 [56] to retrieve GUI layouts and Android Debug Bridge (ADB) [53] to capture screenshots and issue GUI actions, including click, long-click, edit, swipe, and back. The generated properties are translated into the executable format expected by Kea and can be directly executed within its property-based testing workflow.

From Exploration to Specification: LLM-Based Property Generation for Mobile App Testing

Table 1: App subjects used in our experiment (K=1,000, M=1,000,000) App Name OmniNotes Markor RetroMusic Amaze MyExpenses AntennaPod AnkiDroid OuterTune NewPipe MaterialFiles Orgzly uhabits

5

App Feature Note Manager Text Editor Audio Player File Manager Financial Assistant Podcast Manager Flashcards Manager Youtube Music Player Video Player Storage Browser To-do Lists Manager Habit Tracker

#Downloads 100∼500K 1∼5M 1∼5M 1∼5M 1∼5M 10∼50M 1∼5M 100∼500K 5∼10M

#Stars 2.8K 5.3K 5K 6.1K 1.1K 7.7K 10.9K 4.8K 37.5K 8K 2.8K 9.7K

LOC 57,529 79,749 110,065 159,040 317,899 130,925 403,785 89,673 187,187 95,705 72,042 69,652

Evaluation

We evaluate PropGen from four perspectives: functionality exploration and property generation, property refinement, bug detection, and comparison with prior related techniques. Accordingly, we investigate whether PropGen can accurately explore app functionalities and generate semantically correct executable properties, to what extent the generated properties suffer from imprecision that leads to false positives and whether such imprecision can be refined, whether the resulting properties can help uncover new functional bugs in real-world apps, and how PropGen compares with existing functional testing techniques in uncovering such bugs. We formulate the following research questions: • RQ1: How effective is PropGen in exploring app functionalities and generating valid properties? • RQ2: To what extent do generated properties suffer from imprecision that leads to false positives, and how effective is our refinement technique in refining them? • RQ3: Can the generated properties help find new functional bugs in real-world mobile apps? • RQ4: How does PropGen compare with prior functional testing techniques in uncovering new functional bugs?

5.1

Setup and Method

App subjects. We selected 12 popular and representative opensource Android apps as experimental subjects. Among them, eight apps were adopted from prior studies on functional bug detection for Android apps [48, 52, 60, 66]. From the candidate apps used in these studies, we excluded those that were either (1) no longer runnable or actively maintained, or (2) highly similar in functionality to apps already selected. To further improve subject diversity, we additionally included four popular open-source apps from Google Play that provide different features. Table 1 summarizes the selected apps. In the table, App Feature denotes the primary functionality of each app, #Downloads and #Stars report the number of Google Play installations and GitHub stars, respectively, and LOC gives the lines of code. Experimental environment. All experiments were conducted on a machine running Ubuntu 22.04 with 192 CPU cores (AMD EPYC 9654) and official Android emulators (Android 11, Pixel). We use GPT-5.2 as the backend MLLM with default settings for PropGen and baseline tools that involve LLM. For each app, we allocated 3

Conference’17, July 2017, Washington, DC, USA

hours for behavioral evidence construction and property synthesis. After that, we used Kea to perform property-based testing with the generated properties for 6 hours per app, following the testing budget adopted in Kea’s paper [66]. Baselines. We use five baselines for different research questions, according to their evaluation goals. For RQ1, we compare PropGen with DroidAgent [69], a representative LLM-based mobile app functionality exploration approach, which can automatically identify and execute functionalities in mobile apps. For RQ4, which evaluates bug-finding capability, we compare PropGen with four representative prior techniques for Android functional bug detection: Genie [48], Odin [60], PBFDroid [49], and VisionDroid [30]. Among them, Genie and Odin rely on designed automated oracles, PBFDroid is a property-based testing technique for data manipulation functionalities (DMFs), and VisionDroid is an LLM-based multi-agent approach for functional bug detection. Evaluation method of RQ1. RQ1 aims to evaluate whether PropGen can correctly infer and execute app functionalities and synthesize valid properties from the collected behavioral evidence. This evaluation cannot be performed fully automatically, because mobile apps typically lack precise functional specifications. Therefore, we manually assess the validity of both the inferred functionalities and the generated property descriptions, following prior work on functionality-level evaluation beyond structural coverage metrics [6, 69]. The manual evaluation mainly involves two annotators, who are graduate students majoring in software engineering and with at least four years of Android app development experience. Before the annotation, each annotator was given time (at least fifteen minutes) to familiarize themselves with the overall functionalities of every subject app. During this process, annotators also referred to the app’s official introduction page when available, so that the subsequent judgments were made with sufficient understanding of the app’s functionalities. In addition, during annotation, annotators could interact with the running app at any time to verify uncertain cases. For each inferred functionality, we evaluate two aspects. The first is functionality validity, which examines whether the inferred functionality actually exists in the app. Annotators are given the inferred functionality description together with the GUI screenshot from which it was inferred, and determine whether the described functionality is genuinely supported by the interface. The second is execution correctness, which examines whether the system correctly executes the inferred functionality. For each inferred functionality, annotators are provided with the corresponding execution screenshots and interaction events, and judge whether the executed interaction sequence indeed realizes the intended functionality. For each generated property description, we assess its validity from three aspects: (1) whether the precondition appropriately constrains the UI state in which the property should be applied, (2) whether the interaction scenario accurately reflects the user interactions required to perform the functionality, and (3) whether the postcondition correctly captures the observable UI behavior that should hold immediately after the scenario. At the same time, because each property is abstracted from an original functionality execution trace, it should first hold on the source trace from which it is derived. Based on this principle, a property description is considered valid if it faithfully reflects the behavior exhibited in

Conference’17, July 2017, Washington, DC, USA

the source trace and can serve as a reasonable specification of the intended functionality; otherwise, it is labeled as invalid. Two annotators independently performed the annotations. We measured inter-rater agreement using Cohen’s 𝜅, obtaining 0.91, 0.82, and 0.81 for functionality validity, execution correctness, and property validity, respectively. Disagreements were resolved through discussion with authors. Based on these annotations, we report the proportions of inferred functionalities that are valid, inferred functionalities that are correctly executed, and generated property descriptions that are valid. We note that, because mobile apps lack precise functional specifications, manual annotation in RQ1 mainly serves as a sanity check on the validity of the generated property descriptions. Whether these properties are precise as executable specifications still needs to be validated through execution. Therefore, RQ2 further examines their precision by running the translated executable properties and analyzing the reported violations. Evaluation method of RQ2 and RQ3. RQ2 evaluates two aspects of property refinement: (1) how many generated properties are imprecise and thus lead to spurious violations during testing, and (2) how many of these imprecise properties can be successfully refined through refinement. RQ3 evaluates whether the generated properties can uncover new functional bugs. Specifically, for each app, we load all initially generated executable properties into Kea [66] for testing with 6 hours. Whenever Kea reports a property violation, we manually inspect the property description, executable property code, violation-triggering execution trace, corresponding screenshots and interaction events, and the assertion outcome. Based on this, we determine whether the violation is caused by a real app bug or by non-bug factors, such as property imprecision or automation failures. For RQ2, we focus on the properties whose reported violations are diagnosed as spurious. We apply refinement only to those caused by property imprecision. For each such property, the refinement module takes the original property description, executable property code, and violation-triggering execution evidence as input, and produces a revised executable property. We then re-execute the refined property on the app and inspect the result. A refinement is considered successful if the revised property no longer triggers the same spurious violation while preserving the original testing intent. Based on this process, we report the number of properties sent to refinement due to property imprecision, the number and rate of successful refinements, and the breakdown of successfully refined properties by the modified component (i.e., precondition, interaction, and postcondition). For RQ3, we focus on the violations diagnosed as real app bugs through manual inspection. For each confirmed bug, we prepare a bug report containing the bug description, reproduction steps, expected and actual behaviors, and submit it to the corresponding app developers. Evaluation method of RQ4. RQ4 evaluates whether existing functional testing techniques can find the bugs uncovered by PropGen. We emphasize that this comparison is intended to assess complementarity rather than replacement, i.e., whether PropGen can uncover bugs that prior approaches may miss. Following prior comparative analysis practice [66], we evaluate these tools from two perspectives. First, we conduct a scope

Yiheng Xiong, Shiwen Song, Bo Ma, Ting Su, and Xiaofei Xie

Table 2: Validity of behavioral evidence and synthesized properties across subject apps (RQ1). #Inferred Func

#Correctly Executed

#Valid Func

#Prop

#Valid Prop

80 (74.1%)

81

80 (98.8%)

85 (72.6%)

88

83 (94.3%)

88 (77.9%)

89

70 (78.7%)

8 (33.3%)

64 (76.2%)

57

52 (91.2%)

104 (98.1%)

21 (38.9%)

82 (77.4%)

81

78 (96.3%)

38 (80.9%)

139 (97.9%)

28 (73.7%)

116 (81.7%)

120

111 (92.5%)

App Name D

P

D

P

D

OmniNotes

53

108

53 (100.0%)

102 (94.4%)

18 (34.0%)

Markor

48

117

36 (75.0%)

116 (99.1%)

12 (33.3%)

RetroMusic

48

113

42 (87.5%)

104 (92.0%)

9 (21.4%)

Amaze

37

84

24 (64.9%)

83 (98.8%)

MyExpenses

54

106

54 (100.0%)

AntennaPod

47

142

P

AnkiDroid

50

116

28 (56.0%)

107 (92.2%)

9 (32.1%)

93 (80.2%)

91

85 (93.4%)

OuterTune

41

76

41 (100.0%)

67 (88.2%)

9 (22.0%)

55 (72.4%)

48

44 (91.7%)

NewPipe

46

106

45 (97.8%)

92 (86.8%)

20 (44.4%)

81 (76.4%)

79

72 (91.1%)

MaterialFiles

47

110

44 (93.6%)

103 (93.6%)

23 (52.3%)

82 (74.5%)

86

82 (95.3%)

Orgzly

49

124

48 (98.0%)

115 (92.7%)

14 (29.2%)

88 (71.0%)

96

91 (94.8%)

uhabits

55

80

38 (69.1%)

78 (97.5%)

16 (42.1%)

63 (78.8%)

69

64 (92.8%)

Total

575

1282

491 (85.4%)

1210 (94.4%)

187 (35.2%)

977 (76.2%)

985

912 (92.6%)

analysis to determine whether each of the 25 bugs uncovered by PropGen theoretically falls within the detection scope of each prior technique. This analysis is performed manually based on bug characteristics and the detection capabilities claimed by each technique. To improve reliability, we further consulted the authors of Genie, Odin, and PBFDroid to validate our analysis. For VisionDroid, we do not perform a separate scope analysis, since its LLM-based design makes its theoretical detection scope difficult to characterize precisely; instead, we focus only on its empirical bug-finding performance. Second, we empirically evaluate each tool by running it on the corresponding apps and checking whether it can rediscover the same bugs in practice. For Genie, Odin, and VisionDroid, we follow the default configurations described in their original papers. PBFDroid requires users to manually specify properties for data manipulation functionalities (DMFs). Therefore, we manually defined the required DMF properties for detecting the corresponding bugs. To ensure fairness, we align the time budget with each tool’s workflow: PropGen uses 3 hours for property generation and 6 hours for bug finding; accordingly, we allocate 9 hours per app to Genie, Odin, and VisionDroid, and 6 hours of automated testing to PBFDroid after manual property construction.

5.2

Results of RQ1

Table 2 reports the results of functionality inference, execution, and property synthesis on all subject apps, where #Inferred Func denotes the number of functionalities identified by tools, #Valid Func, #Correctly Executed and #Valid Prop denote the numbers of functionalities and properties validated by human annotators, and #Prop denotes the number of generated properties. For functionalityrelated evaluation, we compare DroidAgent (D) and our approach (P). Overall, our approach consistently outperforms DroidAgent in both functionality inference and execution. Across the 12 apps, our approach infers 1,282 functionalities, of which 1,210 are judged valid, achieving 94.4% functionality validity, compared with 575 inferred functionalities and 491 valid ones (85.4%) for DroidAgent. It also correctly executes 977 functionalities, yielding 76.2% execution correctness, substantially higher than DroidAgent’s 187 correctly executed functionalities and 35.2% execution correctness. On average, this corresponds to 101 valid functionalities and 81 correctly

From Exploration to Specification: LLM-Based Property Generation for Mobile App Testing

Table 3: Effectiveness of property refinement across subject apps (RQ2). Modified Component Pre I Post

App Name

#Imprecise Prop

#Successful Refinements

OmniNotes Markor RetroMusic Amaze MyExpenses

12 15 15 11 8

11 (91.7%) 12 (80.0%) 14 (93.3%) 10 (90.9%) 8 (100.0%)

5 2 9 2 6

0 1 0 0 0

6 9 5 8 2

AntennaPod AnkiDroid OuterTune NewPipe MaterialFiles Orgzly uhabits

20 9 3 11 6 12 5

18 (90.0%) 9 (100.0%) 3 (100.0%) 10 (90.9%) 6 (100.0%) 12 (100.0%) 5 (100.0%)

7 7 3 2 2 5 3

0 0 0 0 0 0 0

11 2 0 8 4 7 2

Total

127

118 (92.9%)

53

1

64

Conference’17, July 2017, Washington, DC, USA

Table 4: Statistics of the 25 new functional bugs found by the generated properties. App Name

OmniNotes

RetroMusic

Amaze OuterTune

ID 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25

Violated Property Note info dialog should contain statistical data The date should appear on the selection page The category selection should be changeable The category page should be accessible from the drawer The captured photo should appeared in the note content Returning from the sketch should display the note title The reminder icon should be displayed after setting a reminder The attachment should appear after selection The image can be opened in the note content The FAB should appear after return The specific item should disappear from the list The lyrics should be displayed after saving The item should not exist in the list The image should be displayed after change The artist can be reset to default The metadata should remain consistent The item should be deleted successfully The song list should open from navigation menu The file can be successfully created The item can be found Navigation to the sub-directory should succeed The added number should keep consistent The imported file should be present Star and "Favourite" checkbox should stay in sync The insert image should be displayed after preview

executed functionalities per app for our approach, compared with 41 and 16, respectively, for DroidAgent. One likely reason for the performance gap is the difference in functionality inference. DroidAgent infers functionalities without explicitly grounding them to concrete GUI widgets, making some inferred results loosely related to the current interface context and thus more likely to be invalid or non-executable. In contrast, our approach grounds functionality inference in the current GUI context, which helps produce more valid functionality hypotheses and makes subsequent execution more reliable. Also, we find DroidAgent tends to repeatedly execute failed events during functionality execution. For property synthesis, our approach generates 985 property descriptions, among which 912 are judged valid, corresponding to 92.6% property validity. Moreover, property validity exceeds 90% on most apps, indicating that the synthesized properties are generally well aligned with observed app behaviors. LLM usage cost. For behavioral evidence construction and property synthesis, each LLM call consumes 6,198 tokens / $0.0145 on average. Overall, our approach uses 6,364k tokens / $14.86 per app on average. In comparison, DroidAgent uses 5,109k tokens / $13.01 per app on average.

apps: six apps achieve a 100% refinement rate, while the remaining apps still achieve rates above 80%. We further analyze which property components are modified during refinement. Among the 118 successfully refined properties, 53 involve precondition modifications, 64 involve postcondition modifications, and only 1 involves an interaction modification. This suggests that most false positives can be resolved by refining when a property should be triggered or what outcome it should assert, rather than changing the core interaction sequence. Among the 127 refined properties, 9 remain not refined. We find that 5 of them are caused by incorrect diagnosis of spurious violations, while the others occur because the revised property can no longer remain consistent with the original functionality. Note that for property refinement, each property requires 8,768 tokens / $0.02 on average.

5.3

5.4

Results of RQ2

Table 3 reports the effectiveness of our property refinement technique across all subject apps, including how many generated properties produce false positives during property-based testing, how many are successfully refined, and which property components are modified. Among all generated executable properties, 127 produce spurious violations during testing and are thus identified as imprecise properties that lead to false positives. This result shows that property imprecision is not uncommon in LLM-generated properties, and therefore refinement is necessary to improve their practical usability. Overall, our refinement technique is highly effective. Across all apps, 127 properties are sent to refinement, and 118 of them are successfully refined, yielding an overall refinement rate of 92.9%. Moreover, the refinement performance is consistently strong across

MaterialFiles uhabits Orgzly Markor

Results of RQ3

Table 4 summarizes the bug-finding results, including the app name, bug ID, and the brief description of the violated property. Overall, PropGen uncovered 25 unique previously unknown functional bugs in the latest app versions. Currently, 5 of the reported bugs have been fixed by developers, while the remaining reports are waiting for responses. The discovered bugs cover diverse functionalities (e.g., note management, attachment insertion, content display), suggesting that the generated properties can capture a broad range of behavioral constraints in mobile apps. These bugs typically arise when the actual app behavior deviates from the expected behavior encoded by the generated properties. For example, Bug 5 in OmniNotes is triggered by the property The captured photo should appear in the note content. During testing, it generates a GUI event sequence that

Conference’17, July 2017, Washington, DC, USA

Yiheng Xiong, Shiwen Song, Bo Ma, Ting Su, and Xiaofei Xie

Table 5: Results of prior functional testing tools for finding the new functional bugs. Tool Genie ODIN PBFDroid VisionDroid Total

#New Bugs in Scope 1 (4.0%) 2 (8.0%) 5 (17.9%) 7 (28.0%)

#New Bugs Found 0 (0.0%) 0 (0.0%) 2 (8.0%) 1 (4.0%) 3 (12.0%)

first opens audio recording and then checks this property. After executing the corresponding interaction sequence, the captured photo fails to appear in the note content, thus violating the property. This bug is difficult to uncover through conventional manual testing, as testers typically focus on the main interaction path and may not consider interleavings with other events.

5.5

Results of RQ4

Table 5 summarizes how many of the new bugs found by PropGen can also be detected by Genie, Odin, PBFDroid, and VisionDroid. Among the 25 new bugs uncovered by PropGen, only 7 (28%) are within the scope of these prior techniques, and only 3 (12%) are actually found in practice. This result suggests that PropGen provides complementary bugfinding capability to existing functional testing techniques. We further analysis why most of the bugs cannot be found by prior techniques. Genie, Odin, and PBFDroid are designed with specific types of functional bugs, relying on predefined automated oracles or manually specified DMF properties. As a result, they can only find the bug categories emphasized in their original designs, whereas PropGen targets more broadly through generated properties. VisionDroid, in contrast, is a more general LLM-based functional testing approach. Its exploration strategy typically validates a functionality by following one plausible interaction path at a time. In contrast, most bugs uncovered by PropGen do not appear on such a straightforward execution path. Instead, they are exposed only when the property is checked under specific event sequences. In other words, these bugs are triggered not by whether the main functionality can be completed, but by whether the expected behavior still holds under varied runtime conditions.

6

Threats to Validity

First, our evaluation involves manual inspection to assess the correctness of inferred functionalities and generated properties, which may introduce subjectivity and potential bias. To mitigate this threat, each case is independently labeled by two experienced graduate students following consistent evaluation criteria; disagreements are further discussed until agreement is reached. Second, the apps used in our evaluation may not fully represent the diversity of real-world mobile apps. To mitigate this threat, most of the apps are selected from prior relevant studies, and we further include four additional apps to improve diversity. In the future, we plan to evaluate PropGen on a larger and broader set of apps.

7

Related Work

Automated mobile app GUI testing. Automated testing for mobile apps has been extensively studied. Choudhary et al. [4] conducted a systematic comparison of Android input-generation tools and highlighted both the promise and limitations of automated mobile testing. Prior work has proposed a variety of techniques to automatically explore app GUIs and generate event sequences for detecting crash bugs [8, 17, 29, 31, 33, 38, 47, 58, 61]. For example, Sapienz [33] uses multi-objective search to generate event sequences for improving coverage and exposing crashes. To find non-crash functional bugs, most of prior work [1, 18, 42, 48, 50, 51, 60, 67, 71] designs automated oracles to overcome the oracle problem. However, these work are limited to specific types of functional bugs (e.g., data losses [1, 18, 42, 71]). Some work leverages LLM to analyze GUI pages during exploration to find data inconsistency bugs [19], functional bugs [30], or inconsistencies between app design and implementation [27]. Property-based testing (PBT) is a powerful testing methodology and have been adopted into many different software systems to find logic bugs [2, 5, 20, 21, 23, 32, 35, 37, 43]. Recent work has begun to bring property-based testing to mobile apps. Specifically, PBFDroid [49], PDTDroid [52], and Kea [66] have demonstrated that PBT can be effectively applied to GUI-driven mobile apps and can find non-crashing functional bugs that are difficult for traditional automated GUI testing tools to detect. However, these work still assumes that meaningful properties are manually written by developers or testers. Our work complements these approaches by automating the executable property generation. Automated test generation. Traditional automated test generation techniques, such as fuzzing [34], symbolic execution [14, 45, 54], and search-based testing [12, 36], mainly aim to improve coverage, but often struggle to generate effective assertions [39, 46]. Learningbased approaches leverage pre-trained language models to generate tests from code [25, 55, 68, 70]. Recently, LLMs have shown strong promise in test generation [3, 7, 9, 11, 13, 22, 25, 44, 59, 70]. Beyond unit test generation, several recent studies have explored the use of LLMs in property-related testing tasks. For example, prior work has investigated generating postconditions for individual functions from their comments [10], synthesizing property-based tests from specifications for Python libraries [57], and generating properties for smart contracts [28]. In contrast, our work investigates how LLMs can be used to automatically generate properties for propertybased testing of mobile apps. Recently, different agents have been proposed to automatically perform tasks on mobile apps [40, 41, 62– 64, 69, 72]. These works focus on executing user-provided tasks, whereas our work centers on automatically exploring app functionalities and generating executable properties.

8

Conclusion

In this paper, we present PropGen, an automated approach for constructing properties of mobile apps. By exploring app functionalities and deriving properties from behavioral evidence, PropGen reduces the need for manual property specification. We further propose a feedback-driven refinement technique to refine imprecise properties exposed during testing. Experiments on real-world Android apps show that PropGen can effectively generate correct

From Exploration to Specification: LLM-Based Property Generation for Mobile App Testing

executable properties. These results demonstrate the practical value of automated property construction for mobile app property-based testing.

References [1] Christoffer Quist Adamsen, Gianluca Mezzetti, and Anders Møller. 2015. Systematic execution of android test suites in adverse conditions. In Proceedings of the 2015 International Symposium on Software Testing and Analysis. 83–93. [2] Thomas Arts, John Hughes, Joakim Johansson, and Ulf Wiger. 2006. Testing telecoms software with Quviq QuickCheck. In Proceedings of the 2006 ACM SIGPLAN Workshop on Erlang. 2–10. [3] Yinghao Chen, Zehao Hu, Chen Zhi, Junxiao Han, Shuiguang Deng, and Jianwei Yin. 2024. Chatunitest: A framework for llm-based test generation. In Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering. 572–576. [4] Shauvik Roy Choudhary, Alessandra Gorla, and Alessandro Orso. 2015. Automated test input generation for android: Are we there yet?(e). In 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 429–440. [5] Koen Claessen and John Hughes. 2000. QuickCheck: a lightweight tool for random testing of Haskell programs. In ICFP’00. 268–279. [6] Riccardo Coppola and Emil Alégroth. 2022. A taxonomy of metrics for GUIbased testing research: A systematic literature review. Information and Software Technology 152 (2022), 107062. [7] Yinlin Deng, Chunqiu Steven Xia, Haoran Peng, Chenyuan Yang, and Lingming Zhang. 2023. Large language models are zero-shot fuzzers: Fuzzing deep-learning libraries via large language models. In Proceedings of the 32nd ACM SIGSOFT international symposium on software testing and analysis. 423–435. [8] Zhen Dong, Marcel Böhme, Lucia Cojocaru, and Abhik Roychoudhury. 2020. Time-travel testing of android apps. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering. 481–492. [9] Kohei Dozono, Tiago Espinha Gasiba, and Andrea Stocco. 2024. Large language models for secure code assessment: A multi-language empirical study. arXiv preprint arXiv:2408.06428 (2024). [10] Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, and Shuvendu K Lahiri. 2024. Can large language models transform natural language intent into formal method postconditions? Proceedings of the ACM on Software Engineering 1, FSE (2024), 1889–1912. [11] Angela Fan, Beliz Gokkaya, Mark Harman, Mitya Lyubarskiy, Shubho Sengupta, Shin Yoo, and Jie M Zhang. 2023. Large language models for software engineering: Survey and open problems. In 2023 IEEE/ACM International Conference on Software Engineering: Future of Software Engineering (ICSE-FoSE). IEEE, 31–53. [12] Gordon Fraser and Andrea Arcuri. 2011. Evosuite: automatic test suite generation for object-oriented software. In Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering. 416–419. [13] Cuiyun Gao, Xing Hu, Shan Gao, Xin Xia, and Zhi Jin. 2025. The current challenges of software engineering in the era of large language models. ACM Transactions on Software Engineering and Methodology 34, 5 (2025), 1–30. [14] Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: Directed automated random testing. In Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation. 213–223. [15] Harrison Goldstein, Joseph W Cutler, Daniel Dickstein, Benjamin C Pierce, and Andrew Head. 2024. Property-based testing in practice. In Proceedings of the IEEE/ACM 46th International Conference on Software Engineering. 1–13. [16] Harrison Goldstein, Joseph W Cutler, Adam Stein, Benjamin C Pierce, and Andrew Head. 2022. Some problems with properties. In Proc. Workshop on the Human Aspects of Types and Reasoning Assistants (HATRA), Vol. 1. 3. [17] Tianxiao Gu, Chengnian Sun, Xiaoxing Ma, Chun Cao, Chang Xu, Yuan Yao, Qirun Zhang, Jian Lu, and Zhendong Su. 2019. Practical GUI testing of Android applications via model abstraction and refinement. In 2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE). IEEE, 269–280. [18] Wunan Guo, Zhen Dong, Liwei Shen, Wei Tian, Ting Su, and Xin Peng. 2022. Detecting and fixing data loss issues in Android apps. In ISSTA ’22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis. 605–616. doi:10.1145/3533767.3534402 [19] Yongxiang Hu, Hailiang Jin, Xuan Wang, Jiazhen Gu, Shiyu Guo, Chaoyi Chen, Xin Wang, and Yangfan Zhou. 2024. Autoconsis: Automatic gui-driven data inconsistency detection of mobile apps. In Proceedings of the 46th International Conference on Software Engineering: Software Engineering in Practice. 137–146. [20] John Hughes. 2016. Experiences with QuickCheck: testing the hard stuff and staying sane. In A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. Springer, 169–186. [21] John Hughes, Benjamin C Pierce, Thomas Arts, and Ulf Norell. 2016. Mysteries of dropbox: property-based testing of a distributed synchronization service. In 2016 IEEE International Conference on Software Testing, Verification and Validation (ICST). IEEE, 135–145.

Conference’17, July 2017, Washington, DC, USA

[22] Zongze Jiang, Ming Wen, Jialun Cao, Xuanhua Shi, and Hai Jin. 2024. Towards Understanding the Effectiveness of Large Language Models on Directed Test Input Generation. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering. 1408–1420. [23] Stefan Karlsson, Adnan Čaušević, and Daniel Sundmark. 2020. QuickREST: Property-based test generation of OpenAPI-described RESTful APIs. In 2020 IEEE 13th International Conference on Software Testing, Validation and Verification (ICST). IEEE, 131–141. [24] Pavneet Singh Kochhar, Ferdian Thung, Nachiappan Nagappan, Thomas Zimmermann, and David Lo. 2015. Understanding the test automation culture of app developers. In 2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST). IEEE, 1–10. [25] Shuvendu K Lahiri, Sarah Fakhoury, Aaditya Naik, Georgios Sakkas, Saikat Chakraborty, Madanlal Musuvathi, Piali Choudhury, Curtis von Veh, Jeevana Priya Inala, Chenglong Wang, et al. 2022. Interactive code generation via test-driven user-intent formalization. arXiv preprint arXiv:2208.05950 (2022). [26] Mario Linares-Vásquez, Carlos Bernal-Cárdenas, Kevin Moran, and Denys Poshyvanyk. 2017. How do developers test android applications?. In 2017 IEEE International Conference on Software Maintenance and Evolution (ICSME). IEEE, 613–622. [27] Ruofan Liu, Xiwen Teoh, Yun Lin, Guanjie Chen, Ruofei Ren, Denys Poshyvanyk, and Jin Song Dong. 2025. GUIPilot: A Consistency-Based Mobile GUI Testing Approach for Detecting Application-Specific Bugs. Proceedings of the ACM on Software Engineering 2, ISSTA (2025), 753–776. [28] Ye Liu, Yue Xue, Daoyuan Wu, Yuqiang Sun, Yi Li, Miaolei Shi, and Yang Liu. 2024. Propertygpt: Llm-driven formal verification of smart contracts through retrieval-augmented property generation. arXiv preprint arXiv:2405.02580 (2024). [29] Zhe Liu, Chunyang Chen, Junjie Wang, Mengzhuo Chen, Boyu Wu, Xing Che, Dandan Wang, and Qing Wang. 2024. Make llm a testing expert: Bringing human-like interaction to mobile gui testing via functionality-aware decisions. In Proceedings of the IEEE/ACM 46th International Conference on Software Engineering. 1–13. [30] Zhe Liu, Cheng Li, Chunyang Chen, Junjie Wang, Mengzhuo Chen, Boyu Wu, Yawen Wang, Jun Hu, and Qing Wang. 2025. Seeing is believing: Vision-driven non-crash functional bug detection for mobile apps. IEEE Transactions on Software Engineering (2025). [31] Aravind Machiry, Rohan Tahiliani, and Mayur Naik. 2013. Dynodroid: An input generation system for android apps. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering. 224–234. [32] David R MacIver, Zac Hatfield-Dodds, et al. 2019. Hypothesis: A new approach to property-based testing. Journal of Open Source Software 4, 43 (2019), 1891. [33] Ke Mao, Mark Harman, and Yue Jia. 2016. Sapienz: Multi-objective automated testing for android applications. In Proceedings of the 25th international symposium on software testing and analysis. 94–105. [34] Michał Zalewski. 2016. American Fuzzy Lop - Whitepaper. https://lcamtuf. coredump.cx/afl/technical_details.txt [35] Liam O’Connor and Oskar Wickström. 2022. Quickstrom: property-based acceptance testing with LTL specifications. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI). 1025–1038. doi:10.1145/3519939.3523728 [36] Carlos Pacheco and Michael D Ernst. 2007. Randoop: feedback-directed random testing for Java. In Companion to the 22nd ACM SIGPLAN conference on Objectoriented programming systems and applications companion. 815–816. [37] Rohan Padhye, Caroline Lemieux, and Koushik Sen. 2019. Jqf: Coverage-guided property-based testing in java. In Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. 398–401. [38] Minxue Pan, An Huang, Guoxin Wang, Tian Zhang, and Xuandong Li. 2020. Reinforcement learning based curiosity-driven testing of android applications. In Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis. 153–164. [39] Annibale Panichella, Sebastiano Panichella, Gordon Fraser, Anand Ashok Sawant, and Vincent J Hellendoorn. 2020. Revisiting test smells in automatically generated tests: limitations, pitfalls, and opportunities. In 2020 IEEE international conference on software maintenance and evolution (ICSME). IEEE, 523–533. [40] Yujia Qin, Yining Ye, Junjie Fang, Haoming Wang, Shihao Liang, Shizuo Tian, Junda Zhang, Jiahao Li, Yunxin Li, Shijue Huang, et al. 2025. Ui-tars: Pioneering automated gui interaction with native agents. arXiv preprint arXiv:2501.12326 (2025). [41] Dezhi Ran, Hao Wang, Zihe Song, Mengzhou Wu, Yuan Cao, Ying Zhang, Wei Yang, and Tao Xie. 2024. Guardian: A Runtime Framework for LLM-based UI Exploration. In Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis. [42] Oliviero Riganelli, Simone Paolo Mottadelli, Claudio Rota, Daniela Micucci, and Leonardo Mariani. 2020. Data loss detector: automatically revealing data loss bugs in Android apps. In ISSTA ’20: 29th ACM SIGSOFT International Symposium on Software Testing and Analysis. 141–152. doi:10.1145/3395363.3397379

Conference’17, July 2017, Washington, DC, USA

[43] André Santos, Alcino Cunha, and Nuno Macedo. 2018. Property-based testing for the robot operating system. In Proceedings of the 9th ACM SIGSOFT International Workshop on Automating TEST Case Design, Selection, and Evaluation. 56–62. [44] Max Schäfer, Sarah Nadi, Aryaz Eghbali, and Frank Tip. 2023. An empirical evaluation of using large language models for automated unit test generation. IEEE Transactions on Software Engineering 50, 1 (2023), 85–105. [45] Koushik Sen, Darko Marinov, and Gul Agha. 2005. CUTE: A concolic unit testing engine for C. ACM SIGSOFT software engineering notes 30, 5 (2005), 263–272. [46] Sina Shamshiri. 2015. Automated unit test generation for evolving software. In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering. 1038–1041. [47] Ting Su, Guozhu Meng, Yuting Chen, Ke Wu, Weiming Yang, Yao Yao, Geguang Pu, Yang Liu, and Zhendong Su. 2017. Guided, Stochastic Model-based GUI Testing of Android Apps. In The joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE). 245–256. doi:10.1145/3106237.3106298 [48] Ting Su, Yichen Yan, Jue Wang, Jingling Sun, Yiheng Xiong, Geguang Pu, Ke Wang, and Zhendong Su. 2021. Fully automated functional fuzzing of Android apps for detecting non-crashing logic bugs. Proc. ACM Program. Lang. 5, OOPSLA (2021), 1–31. doi:10.1145/3485533 [49] Jingling Sun, Ting Su, Jiayi Jiang, Jue Wang, Geguang Pu, and Zhendong Su. 2023. Property-Based Fuzzing for Finding Data Manipulation Errors in Android Apps. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE). 1088–1100. doi:10.1145/3611643.3616286 [50] Jingling Sun, Ting Su, Junxin Li, Zhen Dong, Geguang Pu, Tao Xie, and Zhendong Su. 2021. Understanding and finding system setting-related defects in Android apps. In ISSTA ’21: 30th ACM SIGSOFT International Symposium on Software Testing and Analysis. 204–215. doi:10.1145/3460319.3464806 [51] Jingling Sun, Ting Su, Kai Liu, Chao Peng, Zhao Zhang, Geguang Pu, Tao Xie, and Zhendong Su. 2023. Characterizing and Finding System Setting-Related Defects in Android Apps. IEEE Trans. Software Eng. 49, 4 (2023), 2941–2963. doi:10.1109/TSE.2023.3236449 [52] Jingling Sun, Ting Su, Jun Sun, Jianwen Li, Mengfei Wang, and Geguang Pu. 2024. Property-Based Testing for Validating User Privacy-Related Functionalities in Social Media Apps. In Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering. 440–451. [53] Android Team. 2021. Android Debug Bridge (adb). Retrieved 2026-3 from https: //developer.android.com/tools/adb [54] Nikolai Tillmann, Jonathan De Halleux, and Tao Xie. 2014. Transferring an automated test generation tool to practice: From Pex to Fakes and Code Digger. In Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering. 385–396. [55] Michele Tufano, Dawn Drain, Alexey Svyatkovskiy, Shao Kun Deng, and Neel Sundaresan. 2020. Unit test case generation with transformers and focal context. arXiv preprint arXiv:2009.05617 (2020). [56] uiautomator2 Team. 2021. uiautomator2. Retrieved 2026-3 from https://github. com/openatx/uiautomator2 [57] Vasudev Vikram, Caroline Lemieux, Joshua Sunshine, and Rohan Padhye. 2023. Can large language models write good property-based tests? arXiv preprint arXiv:2307.04346 (2023). [58] Chenxu Wang, Tianming Liu, Yanjie Zhao, Minghui Yang, and Haoyu Wang. 2025. Llmdroid: Enhancing automated mobile app gui testing coverage with large language model guidance. Proceedings of the ACM on Software Engineering 2, FSE (2025), 1001–1022. [59] Junjie Wang, Yuchao Huang, Chunyang Chen, Zhe Liu, Song Wang, and Qing Wang. 2024. Software testing with large language models: Survey, landscape, and vision. IEEE Transactions on Software Engineering 50, 4 (2024), 911–936. [60] Jue Wang, Yanyan Jiang, Ting Su, Shaohua Li, Chang Xu, Jian Lu, and Zhendong Su. 2022. Detecting non-crashing functional bugs in Android apps via deepstate differential analysis. In Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE). 434–446. doi:10.1145/3540250.3549170 [61] Jue Wang, Yanyan Jiang, Chang Xu, Chun Cao, Xiaoxing Ma, and Jian Lu. 2020. Combodroid: generating high-quality test inputs for android apps via use case combinations. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering. 469–480. [62] Junyang Wang, Haiyang Xu, Haitao Jia, Xi Zhang, Ming Yan, Weizhou Shen, Ji Zhang, Fei Huang, and Jitao Sang. 2024. Mobile-agent-v2: Mobile device operation assistant with effective navigation via multi-agent collaboration. arXiv preprint arXiv:2406.01014 (2024). [63] Hao Wen, Yuanchun Li, Guohong Liu, Shanhui Zhao, Tao Yu, Toby Jia-Jun Li, Shiqi Jiang, Yunhao Liu, Yaqin Zhang, and Yunxin Liu. 2024. Autodroid: Llm-powered task automation in android. In Proceedings of the 30th Annual International Conference on Mobile Computing and Networking. 543–557. [64] Hao Wen, Hongming Wang, Jiaxuan Liu, and Yuanchun Li. 2023. Droidbot-gpt: Gpt-powered ui automation for android. arXiv preprint arXiv:2304.07061 (2023).

Yiheng Xiong, Shiwen Song, Bo Ma, Ting Su, and Xiaofei Xie

[65] Yiheng Xiong, Ting Su, Jingling Sun, Jue Wang, Qin Li, Geguang Pu, and Zhendong Su. 2026. From Natural Language to Executable Properties for Propertybased Testing of Mobile Apps. arXiv:2603.21263 [cs.SE] https://arxiv.org/abs/ 2603.21263 [66] Yiheng Xiong, Ting Su, Jue Wang, Jingling Sun, Geguang Pu, and Zhendong Su. 2024. General and Practical Property-based Testing for Android Apps. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering. 53–64. [67] Yiheng Xiong, Mengqian Xu, Ting Su, Jingling Sun, Jue Wang, He Wen, Geguang Pu, Jifeng He, and Zhendong Su. 2023. An empirical study of functional bugs in android apps. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA’23). 1319–1331. [68] Lin Yang, Chen Yang, Shutao Gao, Weijing Wang, Bo Wang, Qihao Zhu, Xiao Chu, Jianyi Zhou, Guangtai Liang, Qianxiang Wang, et al. 2024. On the evaluation of large language models in unit test generation. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering. 1607–1619. [69] Juyeon Yoon, Robert Feldt, and Shin Yoo. 2024. Intent-driven mobile gui testing with autonomous large language model agents. In 2024 IEEE Conference on Software Testing, Verification and Validation (ICST). IEEE, 129–139. [70] Zhiqiang Yuan, Mingwei Liu, Shiji Ding, Kaixin Wang, Yixuan Chen, Xin Peng, and Yiling Lou. 2024. Evaluating and improving chatgpt for unit test generation. Proceedings of the ACM on Software Engineering 1, FSE (2024), 1703–1726. [71] Razieh Nokhbeh Zaeem, Mukul R. Prasad, and Sarfraz Khurshid. 2014. Automated Generation of Oracles for Testing User-Interaction Features of Mobile Apps. In Proceedings of the International Conference on Software Testing, Verification and Validation (ICST). 183–192. doi:10.1109/ICST.2014.31 [72] Chi Zhang, Zhao Yang, Jiaxuan Liu, Yanda Li, Yucheng Han, Xin Chen, Zebiao Huang, Bin Fu, and Gang Yu. 2025. Appagent: Multimodal agents as smartphone users. In Proceedings of the 2025 CHI Conference on Human Factors in Computing Systems. 1–20.

Related documents

• Requirements After the First Edit: Mining Late Requirement Emergence and Rework in Real-World Coding-Agent Sessions#639748