                                                   From Exploration to Specification: LLM-Based Property
                                                            Generation for Mobile App Testing
                                                         Yiheng Xiong                                      Shiwen Song                                       Bo Ma
                                              Singapore Management University                  Singapore Management University                  East China Normal University
                                                         Singapore                                        Singapore                                        China
                                                   yihengx98@gmail.com                               swsong@smu.edu.sg                             boma@stu.ecnu.edu.cn

                                                                                      Ting Su                                    Xiaofei Xie
                                                                         East China Normal University                Singapore Management University
                                                                                    China                                       Singapore
arXiv:2604.13463v1 [cs.SE] 15 Apr 2026




                                                                              tsu@sei.ecnu.edu.cn                           xfxie@smu.edu.sg

                                         Abstract                                                                    the functional correctness of mobile apps [24, 26]. However, it is
                                         Mobile apps often suffer from functional bugs that do not cause             brittle, costly to maintain, and typically covers only pre-defined
                                         crashes but instead manifest as incorrect behaviors under specific          happy paths, often missing non-trivial functional bugs [66].
                                         user interactions. Such bugs are difficult to detect by conventional           Property-based testing (PBT) offers a promising direction for
                                         automatic testing techniques because they often lack explicit test          addressing this challenge [5]. Recent work has demonstrated that
                                         oracles. Property-based testing can effectively expose them by spec-        carefully designed properties can reveal non-trivial functional bugs
                                         ifying intended behavior as properties and checking them under              that are missed by other techniques [52, 66]. In mobile app testing,
                                         diverse interactions. However, its practical use is limited by the need     developers specify expected behaviors as properties, and a PBT
                                         for manually written properties, which are difficult and expensive          framework then automatically generates a large number of GUI
                                         to construct.                                                               events to explore diverse GUI states and check whether these prop-
                                            To address this limitation, this paper explores the use of large         erties hold. Compared with validating only a fixed set of manually
                                         language models (LLMs) to automate property construction for                crafted GUI test cases, this paradigm provides a more efficient way
                                         property-based testing of mobile apps. This process is challenging          to assess functional correctness across diverse GUI states.
                                         in two ways. First, it is difficult to systematically uncover and exe-         However, the effectiveness of PBT fundamentally depends on
                                         cute diverse app functionalities. Second, it is difficult to derive valid   the availability of high-quality properties, whose manual construc-
                                         properties from functionality execution results, because a single ex-       tion remains a major barrier to practical adoption [15, 16]. This
                                         ecution provides only limited evidence about what behavior should           challenge is especially pronounced for mobile apps, where explicit
                                         generally hold. To address these challenges, we introduce Prop-             behavioral specifications are often unavailable. As a result, testers
                                         Gen, which performs functionality-guided exploration to collect             must manually understand app functionalities, abstract their ex-
                                         behavioral evidence from execution results, synthesizes properties          pected behaviors into executable properties, and refine the proper-
                                         from the collected evidence, and refines imprecise properties based         ties when reported violations are false positives. This manual and
                                         on testing feedback. We implemented PropGen and evaluated it                iterative process substantially limits the broader adoption of PBT.
                                         on 12 real-world Android apps. The results show that PropGen                   To address this limitation, a promising direction is to leverage
                                         can effectively identify and execute app functionalities, generate          the reasoning and code-generation capabilities of Large Language
                                         valid properties, and refine most imprecise ones. Across all apps,          Models (LLMs) to automate property construction. However, di-
                                         PropGen identified 1,210 valid functionalities and correctly exe-           rectly asking an LLM to generate properties is often unreliable, due
                                         cuted 977 of them, compared with 491 and 187 for the baseline. It           to both the lack of explicit behavioral specifications in mobile apps
                                         generated 985 properties, 912 of which were valid, and successfully         and the tendency of LLMs to hallucinate. Instead, an effective solu-
                                         refined 118 of 127 imprecise ones exposed during testing. Using the         tion should be able to identify app functionalities, infer properties
                                         resulting properties, we found 25 previously unknown functional             from execution-derived behavioral evidence, and refine imprecise
                                         bugs in these apps, many of which were missed by existing testing           properties based on testing feedback.
                                         techniques.                                                                 Challenges. However, achieving this goal is far from straight-
                                                                                                                     forward and presents two key challenges: broad functionality ex-
                                         1    Introduction                                                           ploration and property abstraction from execution traces. First, the
                                         Mobile apps are highly interactive and stateful systems whose func-         approach must explore as many meaningful app functionalities as
                                         tionalities are largely driven by user interface interactions. Despite      possible, but this is difficult in mobile apps. Many functionalities are
                                         extensive testing efforts, functional bugs (e.g., incorrect interaction     not directly visible on the current screen. They may only become
                                         logic) remain prevalent in real-world apps [67]. These bugs often           available after several navigation steps, under specific UI states, or
                                         do not manifest as crashes, making them difficult to detect using           through transient interface elements such as menus and dialogs. As
                                         conventional GUI testing techniques that mainly emphasize code              a result, systematically exposing a large and diverse set of function-
                                         coverage or crash discovery [8, 17, 29, 31, 33, 38, 47, 58, 61]. Manual     alities through app exploration is non-trivial. Without sufficient
                                         testing (e.g., writing GUI tests) is widely used in practice to validate    functionality exposure, the generated properties can cover only
Conference’17, July 2017, Washington, DC, USA                                                 Yiheng Xiong, Shiwen Song, Bo Ma, Ting Su, and Xiaofei Xie


a limited portion of app behavior. Second, even after a function-             In summary, this paper makes the following contributions:
ality is executed, it is still difficult to infer a valid property from
                                                                          • We propose a novel approach that automatically explores app
the execution traces. This is because a property must capture the
                                                                            functionalities and generates properties from runtime behavioral
essential behavior of the functionality, rather than merely describe
                                                                            evidence, without relying on manual specifications.
one observed execution. In practice, however, the execution trace
                                                                          • We design a hypothesis-driven behavioral evidence construction
(e.g., events and screenshots) is often noisy and low-level, and only
                                                                            technique that infers functionalities from GUI states and sum-
provides a single concrete behavioral instance. Moreover, the in-
                                                                            marizes execution traces into structured representations suitable
ferred property can become inaccurate: it may encode details that
                                                                            for property synthesis.
happen to hold in the current trace, but do not necessarily hold in
                                                                          • We develop a property synthesis and refinement approach that
other valid contexts. Such imprecision can lead to false positives
                                                                            derives properties from behavior evidence and refines imprecise
during testing and reduce the usefulness of the generated proper-
                                                                            properties through execution feedback.
ties. Importantly, this difficulty is also faced by human developers
                                                                          • We implement our approach as PropGen and conduct an exten-
when manually writing properties.
                                                                            sive evaluation on 12 real-world Android apps. The results show
Our approach. To address the first challenge, we design a function-
                                                                            that PropGen can cover a large number of app functionalities
ality hypothesis-guided exploration strategy that systematically
                                                                            while achieving high functionality and property validity, and can
uncovers executable app functionalities and collects behavioral evi-
                                                                            effectively refine most imprecise properties.
dence from their executions. Given a GUI state, our approach infers
candidate functionalities and grounds each of them in concrete            2    Background
actionable widgets, making the inferred functionality hypothesis
                                                                          Property-based testing. Property-based testing is a powerful test-
both reliable and directly executable. Based on these hypotheses,
                                                                          ing methodology that validates whether a program satisfies general
our approach performs targeted functionality execution. During
                                                                          properties rather than specific input-output examples [5]. Instead
this process, it incrementally expands the functionality pool when
                                                                          of writing example-based test cases, testers specify high-level prop-
new functionality appears, reuses previously inferred function-
                                                                          erties that describe the expected behavior of the system. Then, a
alities across recurrent GUI states, and falls back to lightweight
                                                                          PBT framework automatically generates a large number of test
random exploration only when no functionality is available. This
                                                                          inputs and executes them to verify whether the properties hold.
hybrid strategy improves functionality coverage and enables richer
                                                                          For example, for a sorting function sort, rather than enumerating
behavioral evidence collection under a limited exploration budget.
                                                                          concrete examples (e.g., sort([3,1,2])== [1,2,3]), one can de-
    To address the second challenge, PropGen adopts property gen-
                                                                          fine a general property such as idempotence: sort(sort(x)) =
eration from behavior evidence followed by feedback-driven re-
                                                                          sort(x). The PBT framework then generates a large number of
finement. Instead of generating properties directly from execution
                                                                          inputs to verify this property and reports any violating input as a
results, PropGen first abstracts each functionality execution trace
                                                                          counterexample.
into a compact condition–action–outcome representation, derives
                                                                          GUI state, event, and functionality. Android applications are
a structured property description, and then translates it into the
                                                                          GUI-driven and event-based. When an app A runs, its runtime
executable property. Because properties inferred from limited evi-
                                                                          state is represented by its current GUI layout, which we denote as a
dence may still over-generalize, PropGen further refines those that
                                                                          GUI state 𝑠. A GUI state corresponds to a hierarchical tree ℓ, whose
trigger false positives during testing. Each refinement is anchored
                                                                          nodes are GUI widgets 𝑤 (e.g., Button, TextView, EditText) with
to the behavioral evidence, allowing PropGen to localize whether
                                                                          attributes (e.g., text, resourceId) and interaction capabilities.
the issue lies in the precondition, interaction, or postcondition
                                                                             User interactions are modeled as events. An event is defined as
and apply a targeted refinement. Through this process, PropGen
                                                                          𝑒 = ⟨𝑡, 𝑤, 𝑑⟩, where 𝑡 is the event type (e.g., click), 𝑤 is the target
improves property precision and robustness while preserving the
                                                                          widget, and 𝑑 is optional data (e.g., text input). An app execution is
original intent.
                                                                          modeled as a sequence of events. Given 𝐸 = [𝑒 1, . . . , 𝑒𝑛 ], executing
Evaluation and results. We implemented our approach as a tool                                            𝑒1              𝑒𝑛
                                                                          A produces a trace 𝜏 = 𝑠 0 −→ 𝑠 1 →   − · · · −−→ 𝑠𝑛 , or 𝑠 0 ⇝ 𝑠𝑛 , where
                                                                                                                                         𝐸
named PropGen and evaluated it on 12 real-world popular and
diverse Android apps. Across all apps, PropGen inferred 1,282 func-       𝑠 0 is the initial state. Then, we define a functionality as a tuple 𝑓 =
tionalities, of which 1,210 (94.4%) were valid and 977 (76.2%) were       ⟨𝑑, 𝜏⟩, where 𝑑 is a semantic intent of a functionality (e.g., "create a
correctly executed. In comparison, the baseline approach inferred         note"), and 𝜏 is an execution trace that realizes this functionality.
575 functionalities, with 491 valid and 187 correctly executed. It fur-   Concretely, 𝜏 has the form 𝑠 ⇝ 𝑠 ′ , where 𝐸 is a sequence of one or
                                                                                                          𝐸

ther generated 985 property descriptions, 912 (92.6%) of which were       more events executable from GUI state 𝑠. Executing 𝜏 completes
valid. During property-based testing, 127 properties were found           the corresponding functionality and produces a concrete effect on
to be imprecise, and 118 (93.7%) of them were successfully refined        the app state.
by our refinement technique. Using the generated properties, we           Property-based testing for mobile apps. In property-based test-
found 25 previously unknown functional bugs in the latest versions        ing for mobile apps, a property specifies an expected behavior of
of the subject apps, whereas existing functional testing techniques       the app. A property can be defined as a tuple 𝜙 = ⟨𝑃, 𝐼, 𝑄⟩, where 𝑃
could find only 3 of them in practice. These results demonstrate          specifies the GUI states where the property applies, 𝐼 is the interac-
the effectiveness of our approach in automating property construc-        tion scenario, and 𝑄 specifies the expected outcome after executing
tion for mobile apps, as well as the bug-finding capability of the        𝐼 . During testing, when a GUI state 𝑠 satisfies 𝑃, the interaction
resulting properties.                                                     scenario 𝐼 is executed from 𝑠 to reach a new state 𝑠 ′ . The property
From Exploration to Specification: LLM-Based Property Generation for Mobile App Testing                                 Conference’17, July 2017, Washington, DC, USA


is satisfied when (𝑠 |= 𝑃 ∧𝑠 ⇝ 𝑠 ′ ) ⇒ 𝑠 ′ |= 𝑄; Otherwise, a property
                                 𝐼
                                                                                          Algorithm 1 Behavioral Evidence Construction
violation is reported.                                                                    Require: Target app A, time budget 𝐵
                                                                                          Ensure: Behavioral evidence set T̂
                                                                                           1: Launch A; obtain initial state 𝑠
3     Approach
                                                                                           2: G𝐹 ← ∅, U ← ∅, T̂ ← ∅
Overview. Given an app, PropGen automatically generates prop-                              3: while elapsed time < 𝐵 do
erties from runtime executions and further refines imprecise ones                          4:    𝑢 (𝑠) ← Extract(𝑠)                         ⊲ Extract the widgets
based on testing feedback. Figure 1 presents the overall workflow,                         5:    if UnseenWidgets(𝑢 (𝑠), U) then
which consists of three stages. First (§3.1), PropGen performs                             6:         𝐹 (𝑠) ← Inferhypothesis(𝑠)           ⊲ infer the hypothesis
hypothesis-driven dynamic exploration to construct behavioral                              7:         G𝐹 ← G𝐹 ∪ 𝐹 (𝑠) ⊲ add the hypothesis into global pool
evidence. For each encountered GUI state 𝑠, it infers functionality                        8:         U ← U ∪ 𝑢 (𝑠)
hypothesis grounded in the visible UI widgets, executes selected                           9:    end if
functionalities, and summarizes the resulting execution traces into                       10:    if HasUnexplored(G𝐹 (𝑢 (𝑠))) then
behavioral evidence for downstream property generation. Second                            11:         𝑓 ← Select(G𝐹 (𝑢 (𝑠)))
(§3.2), PropGen synthesizes properties directly from the behavioral                       12:         (𝜏 𝑓 , 𝑠 ′, G𝐹 , U) ← Execute(𝑓 , 𝑠, G𝐹 , U)
evidence constructed in the first stage. Specifically, it first generates                 13:         T̂ ← T̂ ∪ {Summarize(𝜏 𝑓 )}            ⊲ evidence summary
natural-language property descriptions that capture the intended                          14:         MarkExplored(𝑓 , G𝐹 )
condition–event–outcome relation, and then translates them into                           15:        𝑠 ← 𝑠′
executable properties. Third (§3.3), PropGen validates the gener-                         16:    else
ated properties by the PBT framework and refines properties that                          17:        𝑠 ← RandomExplore(𝑠)
are found to be improperly specified.                                                     18:    end if
Illustrative example. Figure 2 illustrates the workflow of Prop-                          19: end while
Gen on a note-taking app. Starting from the first page in Figure 2                        20: return T̂
(a), PropGen performs behavioral evidence construction by infer-
ring 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.,                              Given a target app A and a time budget 𝐵, PropGen first launches
opening the attachment menu, choosing Camera, taking a photo,                             the app and initializes the global functionality pool G𝐹 , the set of
and returning to the note page. The execution trace is summarized                         observed UI contexts U, and the behavioral evidence set T̂ (Lines 1–
into structured behavioral evidence (as shown in Figure 2(c)), from                       2). It then iteratively explores the app until the budget is exhausted
which PropGen synthesizes an executable property describing the                           (Lines 3–19). In each iteration, PropGen extracts the current GUI
expected behavior of this functionality (Figure 2(d)).                                    context from the current GUI state (Line 4). If the context contains
   The initial synthesized property may be imprecise and thus                             previously unseen widget evidence, PropGen invokes a Multimodal
produce false positives during execution. In this example, its post-                      Large Language Model (MLLM) to infer functionality hypotheses
condition checks whether the app returns to a page containing the                         for the current state, adds them to G𝐹 , and updates U (Lines 5–8).
text “Notes” and whether the newly added attachment is displayed                          PropGen then checks whether the current context contains any
as an attachment thumbnail. This postcondition is too specific. Af-                       unexplored functionality hypothesis (Line 10). If so, it selects one
ter taking a photo, the app may legitimately return to either the                         hypothesis together with its triggering widget, executes it to obtain
Notes page or the Archive page, depending on where the note was                           a functionality trace, and summarizes the trace into a behavioral
opened. Moreover, under reduced view, the attached photo may not                          evidence item added to T̂ (Lines 11–15). Otherwise, PropGen per-
appear as a thumbnail, but instead as a compact attachment icon                           forms lightweight random exploration to leave the current local
(Figure 2(b)). Therefore, the synthesized property may incorrectly                        GUI region and expose new interaction opportunities (Lines 16–
flag a failure even though the photo has been successfully attached.                      17). The process repeats until the time budget is exhausted, after
PropGen then refines the property by relaxing these assertions                            which PropGen returns the collected behavioral evidence set T̂
to allow multiple valid return pages (use the menu button that                            (Lines 19–20).
both pages contain) and attachment representations (thumbnail or
icon). After validating this property using the PBT tool Kea, we                          3.1.1 Functionality Hypothesis Generation. Given a GUI state 𝑠
uncovered a new functional bug: opening audio recording before                            encountered during exploration, this step aims to infer which app
taking a photo prevents the photo attachment from appearing.                              functionalities may be executable under the current interface con-
                                                                                          text. To support subsequent execution, each inferred functionality
                                                                                          is associated with a concrete triggering widget in the current state.
3.1     Behavioral Evidence Construction                                                  Semantic context construction. To support functionality infer-
The goal of this stage is to construct execution-grounded behavioral                      ence, PropGen first constructs a semantic context for the current
evidence for downstream property synthesis. Instead of relying on                         GUI state 𝑠. This context includes three parts: the screen-level con-
external specifications, PropGen systematically explores executable                       text of the current state, app-level semantic cues, and cross-state
app functionalities and records their runtime interaction traces as                       functionality memory. The screen-level context is derived from
behavioral evidence. Algorithm 1 summarizes the workflow.                                 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



                       Behavioral Evidence Construction                                              Property Synthesis from Behaviroal Evidence

                                                                                          Property Description Generation                Executable Property Translation
                         Semantic Context
                                                    Functionality selection
                           Construction

                                                                                                 Feedback-Driven Property Refinement                          Output
                                                      Event Planing and
                       Hypothesis Inference
                                                         Execution                         Executable Property              Validation by PBT tool            Property
                                                                                                                                                             Description
                                                                                                                       Failed Infomation
                                                             Behavioral                                                Imprecise Property
                                                                                                Property
                           Functionality                     Evidence
  App Under Test                                                                               Refinement
                            Hypothesis                     Summarization                                                                                     Executable
                                                                                                                        Failure Evidence                      Property



                                                              Figure 1: Overview of PropGen.




                                                (a) An execution trace of the functionality.                                                    (b) Suspicious violation.
  ① Behavior Evidence Construction



                                                                          ② Property
                                                                              Synthesis
                                                                                                                             ③ Feedback-Driven Property Refinement

                       (c) Behavior evidence.                                                                     (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 visu-                         ⟨𝑓𝑘 , 𝑤𝑘 ⟩], where each functionality hypothesis 𝑓𝑖 is a concise natural-
ally distributed UI elements into explicit references, allowing the                       language description of a candidate app functionality, and 𝑤𝑖 de-
inferred functionalities to be grounded in concrete widgets. The                          notes its corresponding triggering widget. This widget grounding
app-level semantic cues include the app name and the list of activity                     serves two purposes. First, it constrains the MLLM to infer func-
names extracted from the AndroidManifest.xml file, helping the                            tionalities that are supported by the current GUI state, reducing
MLLM interpret the current screen under the broader semantic                              unsupported or non-actionable predictions. Second, it makes the in-
context of A. Finally, the cross-state functionality memory stores                        ferred functionalities directly executable in subsequent exploration.
previously inferred functionalities, helping avoid repeatedly redis-                      The inferred functionality hypothesis, together with their associ-
covering semantically similar functionalities in later GUI states.                        ated triggering widgets, are then stored in the global functionality
Together, these components provide the contextual information                             pool G𝐹 to support later execution and cross-state reuse.
needed for inferring plausible user-facing functionalities from 𝑠.                        Inference triggering and hypothesis reuse. To avoid redun-
Functionality hypothesis inference. Using the constructed se-                             dant MLLM invocations on similar GUI states, PropGen triggers
mantic context, PropGen invokes a MLLM to infer candidate func-                           functionality inference only when a newly visited state introduces
tionality hypothesis for the current GUI state 𝑠. Formally, the in-                       unseen widget evidence. It maintains a global set of explored UI
ferred hypothesis are represented as 𝐹 (𝑠) = [⟨𝑓1, 𝑤 1 ⟩, ⟨𝑓2, 𝑤 2 ⟩, . . . ,             contexts U = {𝑢 1, 𝑢 2, . . .}, where each context is defined as 𝑢 (𝑠) =
From Exploration to Specification: LLM-Based Property Generation for Mobile App Testing                                 Conference’17, July 2017, Washington, DC, USA


⟨𝑎(𝑠),𝑊 (𝑠)⟩, with 𝑎(𝑠) denoting the activity and 𝑊 (𝑠) the set of                        widget 𝑤𝑖 is specified by its numeric label, and 𝑑𝑖 ) specifies the
signatures of leaf-level interactive widgets.                                             attached data (e.g., input text). Before executing 𝑒𝑖 , PropGen ver-
   For each state 𝑠, PropGen compares 𝑊 (𝑠) with existing con-                            ifies that the referenced widget 𝑤𝑖 is present in the current state
texts under the same activity. If no new widget signatures are                            𝑠𝑖 . If the predicted widget identifier is invalid, the event is skipped
observed, it reuses previously inferred functionality hypotheses;                         and directly labeled as a failed step. This guarded execution mecha-
otherwise, it invokes the MLLM to infer new functionalities and                           nism prevents invalid model-predicted interactions and improves
updates the global pool G𝐹 . To enable stable comparison across                           execution robustness.
                                                                                                                                                 𝑒𝑖
screens, each widget 𝑤 is represented by a signature of attributes                             After execution produces a state transition 𝑠𝑖 −→ 𝑠𝑖+1 , PropGen
⟨𝑐𝑙𝑎𝑠𝑠, 𝑟𝑒𝑠𝑜𝑢𝑟𝑐𝑒𝐼𝑑, 𝑡𝑒𝑥𝑡, 𝑑𝑒𝑠𝑐𝑟𝑖𝑝𝑡𝑖𝑜𝑛⟩, which are commonly used to                        evaluates whether the step has advanced the selected functionality.
identify unique widgets in practice [47, 49, 64]. To reduce noise                         This evaluation jointly considers the pre- and post-event GUI states,
from dynamic content, PropGen retains only app-defined text in                            the functionality hypothesis 𝑓 , and the accumulated execution his-
signatures by filtering widget text against a whitelist extracted via                     tory 𝐻𝑖 . Based on this evidence, the MLLM assigns an outcome
static analysis. This avoids treating semantically identical screens                      label 𝑜𝑖 ∈ {success, fail, complete} to the current step. Here, success
with transient text differences as distinct contexts.                                     indicates meaningful progress toward the functionality goal, fail
                                                                                          indicates that the event was unproductive for the intended func-
3.1.2 Hypothesis-Guided Functionality Execution. Given the global                         tionality, and complete indicates that the functionality goal has been
functionality pool G𝐹 generated in § 3.1.1, the goal of this step is                      achieved. The resulting step and outcome are then incorporated
to expand behavioral coverage under a limited exploration budget                          into the execution history for subsequent planning, while complete
by executing app functionalities in a targeted manner. Instead of                         terminates execution of the current functionality.
interacting with A through arbitrary GUI events, PropGen treats                           Behavioral evidence summarization. To support downstream
each functionality hypothesis in G𝐹 , together with its associated                        property synthesis, PropGen summarizes each executed interac-
triggering widget, as an explicit execution target, and prioritizes                       tion trace into compact behavioral evidence. This step is necessary
the execution of previously unexplored functionality hypothesis.                          because raw execution traces are low-level, noisy, and specific to a
   Executing a selected functionality hypothesis ⟨𝑓 , 𝑤⟩ may require                      single execution, whereas property synthesis requires a higher-level
one or more concrete GUI events, thereby inducing state transitions                       representation of the condition–event–outcome relation exhibited
                𝐸
of the form 𝑠 → − 𝑠 ′ . Such functionality-guided execution serves two                    by the app behavior. To bridge this gap, PropGen incrementally
purposes simultaneously: it exercises already identified app behav-                                                           𝑒𝑖
                                                                                          converts each interaction step 𝑠𝑖 −→ 𝑠𝑖+1 into a structured transition
iors to collect behavioral evidence, and it drives the app into new                       with five elements: the state summary before the event, an event
GUI states 𝑠 ′ from which additional functionality hypothesis 𝐹 (𝑠 ′ )                    summary describing the interaction performed, the state summary
can be inferred and inserted into G𝐹 . In this way, execution and                         after the event, a state-diff summary capturing the visible difference
hypothesis generation form a closed exploration loop that progres-                        between the two GUI states, and an outcome label 𝑜𝑖 indicating
sively broadens the functionality space explored by PropGen.                              how the event affected progress toward the selected functionality.
Functionality selection. At each GUI state 𝑠, PropGen retrieves                                The state summaries are functionality-oriented: they describe the
from G𝐹 the candidate functionality hypothesis associated with                            screen context, visible actionable elements, current content state,
the current UI context 𝑢 (𝑠), denoted as G𝐹 (𝑢 (𝑠)). Since the explo-                     and observable feedback cues. In contrast, the state-diff summary
ration budget is limited, PropGen does not execute these candi-                           focuses on the concrete GUI changes induced by the interaction.
dates arbitrarily, but prioritizes those with higher expected explo-                      Together, these summaries preserve the behavioral evidence needed
ration utility. This prioritization is implemented using lightweight                      to capture the executed functionality’s condition–event–outcome
heuristics guided by three considerations: whether the functional-                        relation while filtering out incidental GUI details. The resulting
ity corresponds to a main app behavior, whether it is semantically                        summarized trace, denoted as 𝜏ˆ𝑓 , serves as the behavioral evidence
different from previously executed functionalities, and whether it                        used in the subsequent property synthesis stage.
is likely to be successfully executed in the current context. Based                       Exploration beyond local hypothesis exhaustion. As explo-
on these heuristics, the top-ranked unexplored functionality hy-                          ration proceeds, PropGen may reach GUI states where all available
pothesis ⟨𝑓 , 𝑤⟩ is selected as the next execution target. The selected                   functionality hypothesis have already been executed and no new
hypothesis is then passed to a goal-directed interaction loop that                        hypothesis can be triggered. In such cases, continued MLLM-guided
incrementally plans, executes, and evaluates UI actions until the                         exploration becomes less effective, because the MLLM is most use-
functionality is completed or a step limit is reached.                                    ful when acting toward an explicit functionality goal. When no
Event planning and execution. Once a functionality hypothesis                             such goal is available, the task is no longer to reason about how to
⟨𝑓 , 𝑤⟩ is selected, PropGen executes it through a goal-directed in-                      execute a functionality, but simply to move the app into a new GUI
teraction loop consisting of event planning, guarded execution, and                       region where new functionality hypothesis may emerge. For this
post-event evaluation. At each step 𝑖, PropGen first predicts the                         purpose, lightweight random exploration is both more efficient and
next GUI event based on three sources of information: the function-                       less costly. Therefore, once local functionality-guided exploration is
ality goal 𝑓 , the execution history 𝐻𝑖 of prior events and their out-                    exhausted, PropGen switches to random exploration. It continues
comes, and the current GUI state 𝑠𝑖 , represented as a screenshot with                    traversing the app through random GUI events until it reaches a
labeled widgets. The predicted event is denoted as 𝑒𝑖 = ⟨𝑡𝑖 , 𝑤𝑖 , 𝑑𝑖 ⟩,                  state that either contains unexecuted functionality hypothesis or
where the event type 𝑡𝑖 is chosen from a predefined event space                           exposes unseen widget evidence for new hypothesis generation.
including click, long-click, edit, swipe, and back, the target
Conference’17, July 2017, Washington, DC, USA                                                  Yiheng Xiong, Shiwen Song, Bo Ma, Ting Su, and Xiaofei Xie


In the former case, PropGen resumes functionality-guided execu-            already been made explicit in the preceding natural-language for-
tion directly; in the latter, it first performs functionality hypothesis   mulation step, this translation primarily serves to operationalize the
generation and then continues execution. This design combines              structured specification rather than to perform further behavioral
the strength of goal-directed MLLM-guided execution with the effi-         inference.
ciency of random exploration for escaping locally exhausted GUI               This step is implemented by prompting the LLM with the gen-
regions.                                                                   erated natural-language specification together with framework-
                                                                           specific APIs and widget attributes, with reference to the prompt
3.2     Property Synthesis from Behavior Evidence                          design in prior work on translating natural-language properties
The goal of this stage is to derive executable properties from the         into executable ones [65]. The resulting code is then passed to the
behavioral evidence collected during functionality exploration. As         subsequent validation and refinement stage.
input, PropGen takes the summarized trace 𝜏ˆ𝑓 produced in Sec-
tion 3.1, which compactly captures how a functionality is exercised
and what observable GUI outcome it induces. Each synthesized
                                                                           3.3    Feedback-Driven Property Refinement
property takes the form 𝜙 = ⟨𝑃, 𝐼, 𝑄⟩, where 𝑃 is a precondition, 𝐼        Properties automatically generated from functionality traces may
is an interaction scenario, and 𝑄 is a postcondition assertion.            still be imprecise and therefore trigger false positives during test-
   Rather than generating 𝜙 directly from 𝜏ˆ𝑓 , PropGen decomposes         ing. However, a reported failure should not be refined by simply
property synthesis into two steps, separating semantic property            adapting the property to that single execution, because such a fix
formulation from executable code generation. It first constructs a         may overfit the observed case and drift away from the original
natural-language property specification that explicitly captures the       functionality intent.
intended ⟨𝑃, 𝐼, 𝑄⟩ relation, and then translates this intermediate            Our key idea is that refining a false-positive-inducing property
specification into executable property code.                               requires first recovering the property’s original testing intent, and
Natural-language property description generation. Based on                 then revising it so that it remains valid for both the original intended
the summarized trace 𝜏ˆ𝑓 , PropGen first prompts the MLLM to con-          execution and the newly observed legitimate execution. To this end,
struct a natural-language property specification 𝜙 𝑁 𝐿 = ⟨𝑃, 𝐼, 𝑄⟩ for     we ground refinement in the source summarized trace from which
the functionality captured by the behavioral evidence. The sum-            the property was originally inferred, rather than treating refinement
marized trace provides structured evidence about the execution             as unconstrained rewriting.
context, performed interactions, observable state changes, and step           Specifically, PropGen reasons about the refinement using both
outcomes. Rather than merely restating these observations, the             the source summarized trace and the failure-triggering execution.
MLLM is guided to abstract from 𝜏ˆ𝑓 a generalized behavioral rule          Specifically, it first recovers the original testing intent of the prop-
that should hold across executions of the same functionality.              erty by locating the relevant segment in 𝜏ˆ𝑓 that matches the prop-
   The inferred specification 𝜙 𝑁 𝐿 consists of three parts: a pre-        erty’s triggering context, interaction scenario, and expected out-
condition 𝑃 describing the observable GUI context in which the             come. It then compares this trace-grounded intended behavior with
property should be checked, an interaction scenario 𝐼 capturing the        the failing execution to explain why the violation occurs and iden-
user events needed to exercise the functionality, and a postcondition      tify which component of 𝜙 has become imprecise, i.e., the precon-
𝑄 specifying the immediate visible effect that should hold after-          dition 𝑃, the interaction scenario 𝐼 , or the postcondition 𝑄.
ward. To improve precision and executability, PropGen constrains              Based on this diagnosis, PropGen refines only the faulty compo-
this inference process in three ways. First, 𝑃 must be grounded in         nent through a minimal modification. More specifically, it strength-
observable UI evidence and sufficiently specific to avoid triggering       ens 𝑃 when additional UI guards are needed, revises 𝐼 when the
the property on unrelated screens with superficially similar wid-          event sequence does not faithfully reflect the intended behavior, and
gets. Second, 𝑄 must focus on effects that are directly and reliably       relaxes or simplifies 𝑄 when the assertion is overly specific. In this
verifiable from the GUI, such as the appearance, disappearance, or         way, the refined property remains consistent with both the source-
modification of visible widgets or content. Third, the inferred speci-     trace execution and the newly observed legitimate execution, while
fication should avoid trace-specific brittle details, such as incidental   preserving the original testing intent as much as possible.
text instances or unstable widget states, and instead capture func-
tionality semantics in a form that remains robust across executions.
   In this way, PropGen lifts concrete execution evidence into a           4     Implementation
generalized, testable property abstraction. The resulting natural-         We implemented PropGen as an end-to-end prototype for auto-
language specification makes the intended property semantics ex-           mated property generation on Android apps. The system is pri-
plicit before code generation, thereby separating behavioral under-        marily written in Python and JavaScript, and integrates three key
standing from executable realization.                                      capabilities: GUI state acquisition and interaction, multimodal LLM-
Executable property translation. Given the inferred natural-               based reasoning, and executable property generation for Kea [66].
language property specification 𝜙 𝑁 𝐿 = ⟨𝑃, 𝐼, 𝑄⟩, PropGen trans-          At runtime, PropGen uses uiautomator2 [56] to retrieve GUI layouts
lates it into executable property code for the target PBT frame-           and Android Debug Bridge (ADB) [53] to capture screenshots and
work. Specifically, this step realizes the precondition 𝑃, interaction     issue GUI actions, including click, long-click, edit, swipe, and
scenario 𝐼 , and postcondition 𝑄 using the framework’s property            back. The generated properties are translated into the executable
structure and API conventions, thereby producing a runnable prop-          format expected by Kea and can be directly executed within its
erty implementation. Since the intended property semantics have            property-based testing workflow.
From Exploration to Specification: LLM-Based Property Generation for Mobile App Testing                                 Conference’17, July 2017, Washington, DC, USA


Table 1: App subjects used in our experiment (K=1,000,                                    hours for behavioral evidence construction and property synthesis.
M=1,000,000)                                                                              After that, we used Kea to perform property-based testing with
                                                                                          the generated properties for 6 hours per app, following the testing
    App Name        App Feature            #Downloads       #Stars       LOC              budget adopted in Kea’s paper [66].
    OmniNotes       Note Manager             100∼500K         2.8K      57,529            Baselines. We use five baselines for different research questions,
    Markor          Text Editor                      -        5.3K      79,749
    RetroMusic      Audio Player                 1∼5M           5K     110,065            according to their evaluation goals. For RQ1, we compare Prop-
    Amaze           File Manager                 1∼5M         6.1K     159,040            Gen with DroidAgent [69], a representative LLM-based mobile
    MyExpenses      Financial Assistant          1∼5M         1.1K     317,899            app functionality exploration approach, which can automatically
    AntennaPod      Podcast Manager              1∼5M         7.7K     130,925
    AnkiDroid       Flashcards Manager         10∼50M        10.9K     403,785
                                                                                          identify and execute functionalities in mobile apps. For RQ4, which
    OuterTune       Youtube Music Player             -        4.8K      89,673            evaluates bug-finding capability, we compare PropGen with four
    NewPipe         Video Player                     -       37.5K     187,187            representative prior techniques for Android functional bug detec-
                    Storage Browser              1∼5M           8K      95,705
    MaterialFiles
                                                                                          tion: Genie [48], Odin [60], PBFDroid [49], and VisionDroid [30].
    Orgzly          To-do Lists Manager      100∼500K         2.8K      72,042
    uhabits         Habit Tracker               5∼10M         9.7K      69,652            Among them, Genie and Odin rely on designed automated oracles,
                                                                                          PBFDroid is a property-based testing technique for data manipu-
                                                                                          lation functionalities (DMFs), and VisionDroid is an LLM-based
5      Evaluation                                                                         multi-agent approach for functional bug detection.
We evaluate PropGen from four perspectives: functionality explo-                          Evaluation method of RQ1. RQ1 aims to evaluate whether Prop-
ration and property generation, property refinement, bug detection,                       Gen can correctly infer and execute app functionalities and synthe-
and comparison with prior related techniques. Accordingly, we                             size valid properties from the collected behavioral evidence. This
investigate whether PropGen can accurately explore app func-                              evaluation cannot be performed fully automatically, because mo-
tionalities and generate semantically correct executable properties,                      bile apps typically lack precise functional specifications. Therefore,
to what extent the generated properties suffer from imprecision                           we manually assess the validity of both the inferred functionali-
that leads to false positives and whether such imprecision can be                         ties and the generated property descriptions, following prior work
refined, whether the resulting properties can help uncover new                            on functionality-level evaluation beyond structural coverage met-
functional bugs in real-world apps, and how PropGen compares                              rics [6, 69]. The manual evaluation mainly involves two annotators,
with existing functional testing techniques in uncovering such bugs.                      who are graduate students majoring in software engineering and
We formulate the following research questions:                                            with at least four years of Android app development experience. Be-
                                                                                          fore the annotation, each annotator was given time (at least fifteen
• RQ1: How effective is PropGen in exploring app functionalities
                                                                                          minutes) to familiarize themselves with the overall functionalities
  and generating valid properties?
                                                                                          of every subject app. During this process, annotators also referred
• RQ2: To what extent do generated properties suffer from im-
                                                                                          to the app’s official introduction page when available, so that the
  precision that leads to false positives, and how effective is our
                                                                                          subsequent judgments were made with sufficient understanding of
  refinement technique in refining them?
                                                                                          the app’s functionalities. In addition, during annotation, annotators
• RQ3: Can the generated properties help find new functional bugs
                                                                                          could interact with the running app at any time to verify uncertain
  in real-world mobile apps?
                                                                                          cases.
• RQ4: How does PropGen compare with prior functional testing
                                                                                             For each inferred functionality, we evaluate two aspects. The
  techniques in uncovering new functional bugs?
                                                                                          first is functionality validity, which examines whether the inferred
                                                                                          functionality actually exists in the app. Annotators are given the
5.1       Setup and Method                                                                inferred functionality description together with the GUI screenshot
App subjects. We selected 12 popular and representative open-                             from which it was inferred, and determine whether the described
source Android apps as experimental subjects. Among them, eight                           functionality is genuinely supported by the interface. The second
apps were adopted from prior studies on functional bug detection                          is execution correctness, which examines whether the system cor-
for Android apps [48, 52, 60, 66]. From the candidate apps used                           rectly executes the inferred functionality. For each inferred func-
in these studies, we excluded those that were either (1) no longer                        tionality, annotators are provided with the corresponding execution
runnable or actively maintained, or (2) highly similar in functional-                     screenshots and interaction events, and judge whether the executed
ity to apps already selected. To further improve subject diversity, we                    interaction sequence indeed realizes the intended functionality.
additionally included four popular open-source apps from Google                              For each generated property description, we assess its valid-
Play that provide different features. Table 1 summarizes the selected                     ity from three aspects: (1) whether the precondition appropriately
apps. In the table, App Feature denotes the primary functionality                         constrains the UI state in which the property should be applied,
of each app, #Downloads and #Stars report the number of Google                            (2) whether the interaction scenario accurately reflects the user in-
Play installations and GitHub stars, respectively, and LOC gives the                      teractions required to perform the functionality, and (3) whether
lines of code.                                                                            the postcondition correctly captures the observable UI behavior
Experimental environment. All experiments were conducted on                               that should hold immediately after the scenario. At the same time,
a machine running Ubuntu 22.04 with 192 CPU cores (AMD EPYC                               because each property is abstracted from an original functional-
9654) and official Android emulators (Android 11, Pixel). We use                          ity execution trace, it should first hold on the source trace from
GPT-5.2 as the backend MLLM with default settings for PropGen                             which it is derived. Based on this principle, a property description
and baseline tools that involve LLM. For each app, we allocated 3                         is considered valid if it faithfully reflects the behavior exhibited in
Conference’17, July 2017, Washington, DC, USA                                                         Yiheng Xiong, Shiwen Song, Bo Ma, Ting Su, and Xiaofei Xie


the source trace and can serve as a reasonable specification of the     Table 2: Validity of behavioral evidence and synthesized prop-
intended functionality; otherwise, it is labeled as invalid.            erties across subject apps (RQ1).
   Two annotators independently performed the annotations. We
measured inter-rater agreement using Cohen’s 𝜅, obtaining 0.91,          App Name
                                                                                        #Inferred Func           #Valid Func           #Correctly Executed
                                                                                                                                                                  #Prop
                                                                                                                                                                            #Valid

0.82, and 0.81 for functionality validity, execution correctness, and                   D        P           D                 P          D             P                    Prop

                                                                         OmniNotes      53      108      53 (100.0%)    102 (94.4%)   18 (34.0%)    80 (74.1%)     81     80 (98.8%)
property validity, respectively. Disagreements were resolved through      Markor        48      117      36 (75.0%)     116 (99.1%)   12 (33.3%)    85 (72.6%)     88     83 (94.3%)
discussion with authors. Based on these annotations, we report           RetroMusic     48      113      42 (87.5%)     104 (92.0%)    9 (21.4%)    88 (77.9%)     89     70 (78.7%)

the proportions of inferred functionalities that are valid, inferred       Amaze        37      84       24 (64.9%)     83 (98.8%)     8 (33.3%)    64 (76.2%)     57     52 (91.2%)
                                                                                        54      106      54 (100.0%)    104 (98.1%)   21 (38.9%)    82 (77.4%)     81     78 (96.3%)
functionalities that are correctly executed, and generated property
                                                                         MyExpenses
                                                                         AntennaPod     47      142      38 (80.9%)     139 (97.9%)   28 (73.7%)    116 (81.7%)    120    111 (92.5%)
descriptions that are valid.                                             AnkiDroid      50      116      28 (56.0%)     107 (92.2%)    9 (32.1%)    93 (80.2%)     91     85 (93.4%)
   We note that, because mobile apps lack precise functional speci-      OuterTune      41      76       41 (100.0%)    67 (88.2%)     9 (22.0%)    55 (72.4%)     48     44 (91.7%)

fications, manual annotation in RQ1 mainly serves as a sanity check       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%)
on the validity of the generated property descriptions. Whether            Orgzly       49      124      48 (98.0%)     115 (92.7%)   14 (29.2%)    88 (71.0%)     96     91 (94.8%)
these properties are precise as executable specifications still needs     uhabits       55      80       38 (69.1%)     78 (97.5%)    16 (42.1%)    63 (78.8%)     69     64 (92.8%)

to be validated through execution. Therefore, RQ2 further examines         Total        575    1282      491 (85.4%)   1210 (94.4%)   187 (35.2%)   977 (76.2%)    985    912 (92.6%)

their precision by running the translated executable properties and
analyzing the reported violations.
Evaluation method of RQ2 and RQ3. RQ2 evaluates two aspects             analysis to determine whether each of the 25 bugs uncovered by
of property refinement: (1) how many generated properties are im-       PropGen theoretically falls within the detection scope of each prior
precise and thus lead to spurious violations during testing, and (2)    technique. This analysis is performed manually based on bug char-
how many of these imprecise properties can be successfully refined      acteristics and the detection capabilities claimed by each technique.
through refinement. RQ3 evaluates whether the generated proper-         To improve reliability, we further consulted the authors of Genie,
ties can uncover new functional bugs. Specifically, for each app, we    Odin, and PBFDroid to validate our analysis. For VisionDroid, we
load all initially generated executable properties into Kea [66] for    do not perform a separate scope analysis, since its LLM-based de-
testing with 6 hours. Whenever Kea reports a property violation,        sign makes its theoretical detection scope difficult to characterize
we manually inspect the property description, executable property       precisely; instead, we focus only on its empirical bug-finding per-
code, violation-triggering execution trace, corresponding screen-       formance.
shots and interaction events, and the assertion outcome. Based on          Second, we empirically evaluate each tool by running it on the
this, we determine whether the violation is caused by a real app bug    corresponding apps and checking whether it can rediscover the
or by non-bug factors, such as property imprecision or automation       same bugs in practice. For Genie, Odin, and VisionDroid, we fol-
failures.                                                               low the default configurations described in their original papers.
   For RQ2, we focus on the properties whose reported violations        PBFDroid requires users to manually specify properties for data
are diagnosed as spurious. We apply refinement only to those caused     manipulation functionalities (DMFs). Therefore, we manually de-
by property imprecision. For each such property, the refinement         fined the required DMF properties for detecting the corresponding
module takes the original property description, executable property     bugs. To ensure fairness, we align the time budget with each tool’s
code, and violation-triggering execution evidence as input, and         workflow: PropGen uses 3 hours for property generation and 6
produces a revised executable property. We then re-execute the          hours for bug finding; accordingly, we allocate 9 hours per app to
refined property on the app and inspect the result. A refinement        Genie, Odin, and VisionDroid, and 6 hours of automated testing to
is considered successful if the revised property no longer triggers     PBFDroid after manual property construction.
the same spurious violation while preserving the original testing
intent. Based on this process, we report the number of properties       5.2         Results of RQ1
sent to refinement due to property imprecision, the number and          Table 2 reports the results of functionality inference, execution,
rate of successful refinements, and the breakdown of successfully       and property synthesis on all subject apps, where #Inferred Func
refined properties by the modified component (i.e., precondition,       denotes the number of functionalities identified by tools, #Valid
interaction, and postcondition).                                        Func, #Correctly Executed and #Valid Prop denote the numbers of
   For RQ3, we focus on the violations diagnosed as real app bugs       functionalities and properties validated by human annotators, and
through manual inspection. For each confirmed bug, we prepare           #Prop denotes the number of generated properties. For functionality-
a bug report containing the bug description, reproduction steps,        related evaluation, we compare DroidAgent (D) and our approach
expected and actual behaviors, and submit it to the corresponding       (P). Overall, our approach consistently outperforms DroidAgent
app developers.                                                         in both functionality inference and execution. Across the 12 apps,
Evaluation method of RQ4. RQ4 evaluates whether existing                our approach infers 1,282 functionalities, of which 1,210 are judged
functional testing techniques can find the bugs uncovered by Prop-      valid, achieving 94.4% functionality validity, compared with 575
Gen. We emphasize that this comparison is intended to assess            inferred functionalities and 491 valid ones (85.4%) for DroidAgent. It
complementarity rather than replacement, i.e., whether PropGen          also correctly executes 977 functionalities, yielding 76.2% execution
can uncover bugs that prior approaches may miss.                        correctness, substantially higher than DroidAgent’s 187 correctly
   Following prior comparative analysis practice [66], we evalu-        executed functionalities and 35.2% execution correctness. On aver-
ate these tools from two perspectives. First, we conduct a scope        age, this corresponds to 101 valid functionalities and 81 correctly
From Exploration to Specification: LLM-Based Property Generation for Mobile App Testing                                       Conference’17, July 2017, Washington, DC, USA


Table 3: Effectiveness of property refinement across subject                              Table 4: Statistics of the 25 new functional bugs found by the
apps (RQ2).                                                                               generated properties.

                                                               Modified Component          App Name        ID    Violated Property
   App Name        #Imprecise Prop   #Successful Refinements
                                                               Pre     I    Post                            1     Note info dialog should contain statistical data
   OmniNotes             12                 11 (91.7%)         5      0      6                              2    The date should appear on the selection page
    Markor               15                 12 (80.0%)         2      1      9                              3     The category selection should be changeable
   RetroMusic            15                 14 (93.3%)         9      0      5                              4    The category page should be accessible from the drawer
     Amaze               11                 10 (90.9%)         2      0      8                              5     The captured photo should appeared in the note content
   MyExpenses            8                  8 (100.0%)         6      0      2             OmniNotes
                                                                                                            6    Returning from the sketch should display the note title
   AntennaPod            20                18 (90.0%)          7      0      11                             7     The reminder icon should be displayed after setting a reminder
    AnkiDroid            9                 9 (100.0%)          7      0      2
                                                                                                            8    The attachment should appear after selection
    OuterTune            3                 3 (100.0%)          3      0      0
                                                                                                            9     The image can be opened in the note content
     NewPipe             11                10 (90.9%)          2      0      8
                                                                                                           10    The FAB should appear after return
   MaterialFiles         6                 6 (100.0%)          2      0      4
                                                                                                            11    The specific item should disappear from the list
      Orgzly             12                12 (100.0%)         5      0      7
                                                                                                           12    The lyrics should be displayed after saving
     uhabits             5                 5 (100.0%)          3      0      2
                                                                                                            13    The item should not exist in the list
      Total             127                118 (92.9%)         53     1      64            RetroMusic
                                                                                                           14    The image should be displayed after change
                                                                                                            15    The artist can be reset to default
                                                                                                           16    The metadata should remain consistent
                                                                                             Amaze          17    The item should be deleted successfully
                                                                                                           18    The song list should open from navigation menu
executed functionalities per app for our approach, compared with                            OuterTune
                                                                                                            19    The file can be successfully created
41 and 16, respectively, for DroidAgent.                                                   MaterialFiles   20    The item can be found
   One likely reason for the performance gap is the difference in                                           21    Navigation to the sub-directory should succeed
functionality inference. DroidAgent infers functionalities without                            uhabits      22    The added number should keep consistent
explicitly grounding them to concrete GUI widgets, making some                                Orgzly       23     The imported file should be present
inferred results loosely related to the current interface context and                         Markor       24    Star and "Favourite" checkbox should stay in sync
                                                                                                           25    The insert image should be displayed after preview
thus more likely to be invalid or non-executable. In contrast, our
approach grounds functionality inference in the current GUI con-
text, which helps produce more valid functionality hypotheses and                         apps: six apps achieve a 100% refinement rate, while the remaining
makes subsequent execution more reliable. Also, we find DroidA-                           apps still achieve rates above 80%.
gent tends to repeatedly execute failed events during functionality                          We further analyze which property components are modified
execution.                                                                                during refinement. Among the 118 successfully refined properties,
   For property synthesis, our approach generates 985 property                            53 involve precondition modifications, 64 involve postcondition
descriptions, among which 912 are judged valid, corresponding to                          modifications, and only 1 involves an interaction modification. This
92.6% property validity. Moreover, property validity exceeds 90% on                       suggests that most false positives can be resolved by refining when
most apps, indicating that the synthesized properties are generally                       a property should be triggered or what outcome it should assert,
well aligned with observed app behaviors.                                                 rather than changing the core interaction sequence. Among the
LLM usage cost. For behavioral evidence construction and property                         127 refined properties, 9 remain not refined. We find that 5 of them
synthesis, each LLM call consumes 6,198 tokens / $0.0145 on average.                      are caused by incorrect diagnosis of spurious violations, while the
Overall, our approach uses 6,364k tokens / $14.86 per app on average.                     others occur because the revised property can no longer remain
In comparison, DroidAgent uses 5,109k tokens / $13.01 per app on                          consistent with the original functionality. Note that for property
average.                                                                                  refinement, each property requires 8,768 tokens / $0.02 on average.

5.3      Results of RQ2                                                                   5.4     Results of RQ3
Table 3 reports the effectiveness of our property refinement tech-                        Table 4 summarizes the bug-finding results, including the app name,
nique across all subject apps, including how many generated prop-                         bug ID, and the brief description of the violated property. Overall,
erties produce false positives during property-based testing, how                         PropGen uncovered 25 unique previously unknown functional
many are successfully refined, and which property components are                          bugs in the latest app versions. Currently, 5 of the reported bugs
modified.                                                                                 have been fixed by developers, while the remaining reports are
    Among all generated executable properties, 127 produce spuri-                         waiting for responses.
ous violations during testing and are thus identified as imprecise                           The discovered bugs cover diverse functionalities (e.g., note man-
properties that lead to false positives. This result shows that prop-                     agement, attachment insertion, content display), suggesting that
erty imprecision is not uncommon in LLM-generated properties,                             the generated properties can capture a broad range of behavioral
and therefore refinement is necessary to improve their practical us-                      constraints in mobile apps. These bugs typically arise when the
ability. Overall, our refinement technique is highly effective. Across                    actual app behavior deviates from the expected behavior encoded
all apps, 127 properties are sent to refinement, and 118 of them are                      by the generated properties. For example, Bug 5 in OmniNotes is
successfully refined, yielding an overall refinement rate of 92.9%.                       triggered by the property The captured photo should appear in the
Moreover, the refinement performance is consistently strong across                        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           7    Related Work
the new functional bugs.
                                                                         Automated mobile app GUI testing. Automated testing for mo-
                                                                         bile apps has been extensively studied. Choudhary et al. [4] con-
          Tool            #New Bugs in Scope    #New Bugs Found          ducted a systematic comparison of Android input-generation tools
         Genie                  1 (4.0%)             0 (0.0%)
          ODIN                  2 (8.0%)             0 (0.0%)
                                                                         and highlighted both the promise and limitations of automated
       PBFDroid                5 (17.9%)             2 (8.0%)            mobile testing. Prior work has proposed a variety of techniques
      VisionDroid                   -                1 (4.0%)            to automatically explore app GUIs and generate event sequences
          Total               7 (28.0%)             3 (12.0%)            for detecting crash bugs [8, 17, 29, 31, 33, 38, 47, 58, 61]. For ex-
                                                                         ample, 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 prob-
first opens audio recording and then checks this property. After         lem. However, these work are limited to specific types of functional
executing the corresponding interaction sequence, the captured           bugs (e.g., data losses [1, 18, 42, 71]). Some work leverages LLM to
photo fails to appear in the note content, thus violating the prop-      analyze GUI pages during exploration to find data inconsistency
erty. This bug is difficult to uncover through conventional manual       bugs [19], functional bugs [30], or inconsistencies between app
testing, as testers typically focus on the main interaction path and     design and implementation [27].
may not consider interleavings with other events.                           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
5.5     Results of RQ4                                                   begun to bring property-based testing to mobile apps. Specifically,
Table 5 summarizes how many of the new bugs found by PropGen             PBFDroid [49], PDTDroid [52], and Kea [66] have demonstrated
can also be detected by Genie, Odin, PBFDroid, and VisionDroid.          that PBT can be effectively applied to GUI-driven mobile apps
Among the 25 new bugs uncovered by PropGen, only 7 (28%) are             and can find non-crashing functional bugs that are difficult for
within the scope of these prior techniques, and only 3 (12%) are         traditional automated GUI testing tools to detect. However, these
actually found in practice.                                              work still assumes that meaningful properties are manually written
    This result suggests that PropGen provides complementary bug-        by developers or testers. Our work complements these approaches
finding capability to existing functional testing techniques. We         by automating the executable property generation.
further analysis why most of the bugs cannot be found by prior           Automated test generation. Traditional automated test genera-
techniques. Genie, Odin, and PBFDroid are designed with specific         tion techniques, such as fuzzing [34], symbolic execution [14, 45, 54],
types of functional bugs, relying on predefined automated oracles or     and search-based testing [12, 36], mainly aim to improve coverage,
manually specified DMF properties. As a result, they can only find       but often struggle to generate effective assertions [39, 46]. Learning-
the bug categories emphasized in their original designs, whereas         based approaches leverage pre-trained language models to generate
PropGen targets more broadly through generated properties. Vi-           tests from code [25, 55, 68, 70]. Recently, LLMs have shown strong
sionDroid, in contrast, is a more general LLM-based functional           promise in test generation [3, 7, 9, 11, 13, 22, 25, 44, 59, 70]. Beyond
testing approach. Its exploration strategy typically validates a func-   unit test generation, several recent studies have explored the use
tionality by following one plausible interaction path at a time. In      of LLMs in property-related testing tasks. For example, prior work
contrast, most bugs uncovered by PropGen do not appear on such           has investigated generating postconditions for individual functions
a straightforward execution path. Instead, they are exposed only         from their comments [10], synthesizing property-based tests from
when the property is checked under specific event sequences. In          specifications for Python libraries [57], and generating properties
other words, these bugs are triggered not by whether the main func-      for smart contracts [28]. In contrast, our work investigates how
tionality can be completed, but by whether the expected behavior         LLMs can be used to automatically generate properties for property-
still holds under varied runtime conditions.                             based 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,
6     Threats to Validity
                                                                         whereas our work centers on automatically exploring app function-
First, our evaluation involves manual inspection to assess the cor-      alities and generating executable properties.
rectness 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 grad-      8    Conclusion
uate students following consistent evaluation criteria; disagree-        In this paper, we present PropGen, an automated approach for
ments are further discussed until agreement is reached. Second, the      constructing properties of mobile apps. By exploring app function-
apps used in our evaluation may not fully represent the diversity        alities and deriving properties from behavioral evidence, PropGen
of real-world mobile apps. To mitigate this threat, most of the apps     reduces the need for manual property specification. We further
are selected from prior relevant studies, and we further include         propose a feedback-driven refinement technique to refine impre-
four additional apps to improve diversity. In the future, we plan to     cise properties exposed during testing. Experiments on real-world
evaluate PropGen on a larger and broader set of apps.                    Android apps show that PropGen can effectively generate correct
From Exploration to Specification: LLM-Based Property Generation for Mobile App Testing                                          Conference’17, July 2017, Washington, DC, USA


executable properties. These results demonstrate the practical value                       [22] Zongze Jiang, Ming Wen, Jialun Cao, Xuanhua Shi, and Hai Jin. 2024. Towards
of automated property construction for mobile app property-based                                Understanding the Effectiveness of Large Language Models on Directed Test
                                                                                                Input Generation. In Proceedings of the 39th IEEE/ACM International Conference
testing.                                                                                        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
References                                                                                      IEEE 13th International Conference on Software Testing, Validation and Verification
 [1] Christoffer Quist Adamsen, Gianluca Mezzetti, and Anders Møller. 2015. System-             (ICST). IEEE, 131–141.
     atic execution of android test suites in adverse conditions. In Proceedings of the    [24] Pavneet Singh Kochhar, Ferdian Thung, Nachiappan Nagappan, Thomas Zim-
     2015 International Symposium on Software Testing and Analysis. 83–93.                      mermann, and David Lo. 2015. Understanding the test automation culture of
 [2] Thomas Arts, John Hughes, Joakim Johansson, and Ulf Wiger. 2006. Testing                   app developers. In 2015 IEEE 8th International Conference on Software Testing,
     telecoms software with Quviq QuickCheck. In Proceedings of the 2006 ACM                    Verification and Validation (ICST). IEEE, 1–10.
     SIGPLAN Workshop on Erlang. 2–10.                                                     [25] Shuvendu K Lahiri, Sarah Fakhoury, Aaditya Naik, Georgios Sakkas, Saikat
 [3] Yinghao Chen, Zehao Hu, Chen Zhi, Junxiao Han, Shuiguang Deng, and Jianwei                 Chakraborty, Madanlal Musuvathi, Piali Choudhury, Curtis von Veh, Jee-
     Yin. 2024. Chatunitest: A framework for llm-based test generation. In Compan-              vana Priya Inala, Chenglong Wang, et al. 2022. Interactive code generation
     ion Proceedings of the 32nd ACM International Conference on the Foundations of             via test-driven user-intent formalization. arXiv preprint arXiv:2208.05950 (2022).
     Software Engineering. 572–576.                                                        [26] Mario Linares-Vásquez, Carlos Bernal-Cárdenas, Kevin Moran, and Denys Poshy-
 [4] Shauvik Roy Choudhary, Alessandra Gorla, and Alessandro Orso. 2015. Au-                    vanyk. 2017. How do developers test android applications?. In 2017 IEEE In-
     tomated test input generation for android: Are we there yet?(e). In 2015 30th              ternational Conference on Software Maintenance and Evolution (ICSME). IEEE,
     IEEE/ACM International Conference on Automated Software Engineering (ASE).                 613–622.
     IEEE, 429–440.                                                                        [27] Ruofan Liu, Xiwen Teoh, Yun Lin, Guanjie Chen, Ruofei Ren, Denys Poshyvanyk,
 [5] Koen Claessen and John Hughes. 2000. QuickCheck: a lightweight tool for                    and Jin Song Dong. 2025. GUIPilot: A Consistency-Based Mobile GUI Testing
     random testing of Haskell programs. In ICFP’00. 268–279.                                   Approach for Detecting Application-Specific Bugs. Proceedings of the ACM on
 [6] Riccardo Coppola and Emil Alégroth. 2022. A taxonomy of metrics for GUI-                   Software Engineering 2, ISSTA (2025), 753–776.
     based testing research: A systematic literature review. Information and Software      [28] Ye Liu, Yue Xue, Daoyuan Wu, Yuqiang Sun, Yi Li, Miaolei Shi, and Yang Liu.
     Technology 152 (2022), 107062.                                                             2024. Propertygpt: Llm-driven formal verification of smart contracts through
 [7] Yinlin Deng, Chunqiu Steven Xia, Haoran Peng, Chenyuan Yang, and Lingming                  retrieval-augmented property generation. arXiv preprint arXiv:2405.02580 (2024).
     Zhang. 2023. Large language models are zero-shot fuzzers: Fuzzing deep-learning       [29] Zhe Liu, Chunyang Chen, Junjie Wang, Mengzhuo Chen, Boyu Wu, Xing Che,
     libraries via large language models. In Proceedings of the 32nd ACM SIGSOFT                Dandan Wang, and Qing Wang. 2024. Make llm a testing expert: Bringing
     international symposium on software testing and analysis. 423–435.                         human-like interaction to mobile gui testing via functionality-aware decisions. In
 [8] Zhen Dong, Marcel Böhme, Lucia Cojocaru, and Abhik Roychoudhury. 2020.                     Proceedings of the IEEE/ACM 46th International Conference on Software Engineering.
     Time-travel testing of android apps. In Proceedings of the ACM/IEEE 42nd Inter-            1–13.
     national Conference on Software Engineering. 481–492.                                 [30] Zhe Liu, Cheng Li, Chunyang Chen, Junjie Wang, Mengzhuo Chen, Boyu Wu,
 [9] Kohei Dozono, Tiago Espinha Gasiba, and Andrea Stocco. 2024. Large language                Yawen Wang, Jun Hu, and Qing Wang. 2025. Seeing is believing: Vision-driven
     models for secure code assessment: A multi-language empirical study. arXiv                 non-crash functional bug detection for mobile apps. IEEE Transactions on Software
     preprint arXiv:2408.06428 (2024).                                                          Engineering (2025).
[10] Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, and Shuvendu K Lahiri.           [31] Aravind Machiry, Rohan Tahiliani, and Mayur Naik. 2013. Dynodroid: An input
     2024. Can large language models transform natural language intent into formal              generation system for android apps. In Proceedings of the 2013 9th Joint Meeting
     method postconditions? Proceedings of the ACM on Software Engineering 1, FSE               on Foundations of Software Engineering. 224–234.
     (2024), 1889–1912.                                                                    [32] David R MacIver, Zac Hatfield-Dodds, et al. 2019. Hypothesis: A new approach
[11] Angela Fan, Beliz Gokkaya, Mark Harman, Mitya Lyubarskiy, Shubho Sengupta,                 to property-based testing. Journal of Open Source Software 4, 43 (2019), 1891.
     Shin Yoo, and Jie M Zhang. 2023. Large language models for software engineering:      [33] Ke Mao, Mark Harman, and Yue Jia. 2016. Sapienz: Multi-objective automated
     Survey and open problems. In 2023 IEEE/ACM International Conference on Software            testing for android applications. In Proceedings of the 25th international symposium
     Engineering: Future of Software Engineering (ICSE-FoSE). IEEE, 31–53.                      on software testing and analysis. 94–105.
[12] Gordon Fraser and Andrea Arcuri. 2011. Evosuite: automatic test suite generation      [34] Michał Zalewski. 2016. American Fuzzy Lop - Whitepaper. https://lcamtuf.
     for object-oriented software. In Proceedings of the 19th ACM SIGSOFT symposium             coredump.cx/afl/technical_details.txt
     and the 13th European conference on Foundations of software engineering. 416–419.     [35] Liam O’Connor and Oskar Wickström. 2022. Quickstrom: property-based accep-
[13] Cuiyun Gao, Xing Hu, Shan Gao, Xin Xia, and Zhi Jin. 2025. The current chal-               tance testing with LTL specifications. In Proceedings of the 43rd ACM SIGPLAN
     lenges of software engineering in the era of large language models. ACM Trans-             International Conference on Programming Language Design and Implementation
     actions on Software Engineering and Methodology 34, 5 (2025), 1–30.                        (PLDI). 1025–1038. doi:10.1145/3519939.3523728
[14] Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: Directed auto-         [36] Carlos Pacheco and Michael D Ernst. 2007. Randoop: feedback-directed random
     mated random testing. In Proceedings of the 2005 ACM SIGPLAN conference on                 testing for Java. In Companion to the 22nd ACM SIGPLAN conference on Object-
     Programming language design and implementation. 213–223.                                   oriented programming systems and applications companion. 815–816.
[15] Harrison Goldstein, Joseph W Cutler, Daniel Dickstein, Benjamin C Pierce, and         [37] Rohan Padhye, Caroline Lemieux, and Koushik Sen. 2019. Jqf: Coverage-guided
     Andrew Head. 2024. Property-based testing in practice. In Proceedings of the               property-based testing in java. In Proceedings of the 28th ACM SIGSOFT Interna-
     IEEE/ACM 46th International Conference on Software Engineering. 1–13.                      tional Symposium on Software Testing and Analysis. 398–401.
[16] Harrison Goldstein, Joseph W Cutler, Adam Stein, Benjamin C Pierce, and Andrew        [38] Minxue Pan, An Huang, Guoxin Wang, Tian Zhang, and Xuandong Li. 2020.
     Head. 2022. Some problems with properties. In Proc. Workshop on the Human                  Reinforcement learning based curiosity-driven testing of android applications.
     Aspects of Types and Reasoning Assistants (HATRA), Vol. 1. 3.                              In Proceedings of the 29th ACM SIGSOFT International Symposium on Software
[17] Tianxiao Gu, Chengnian Sun, Xiaoxing Ma, Chun Cao, Chang Xu, Yuan Yao,                     Testing and Analysis. 153–164.
     Qirun Zhang, Jian Lu, and Zhendong Su. 2019. Practical GUI testing of An-             [39] Annibale Panichella, Sebastiano Panichella, Gordon Fraser, Anand Ashok Sawant,
     droid applications via model abstraction and refinement. In 2019 IEEE/ACM 41st             and Vincent J Hellendoorn. 2020. Revisiting test smells in automatically generated
     International Conference on Software Engineering (ICSE). IEEE, 269–280.                    tests: limitations, pitfalls, and opportunities. In 2020 IEEE international conference
[18] Wunan Guo, Zhen Dong, Liwei Shen, Wei Tian, Ting Su, and Xin Peng. 2022.                   on software maintenance and evolution (ICSME). IEEE, 523–533.
     Detecting and fixing data loss issues in Android apps. In ISSTA ’22: 31st ACM         [40] Yujia Qin, Yining Ye, Junjie Fang, Haoming Wang, Shihao Liang, Shizuo Tian,
     SIGSOFT International Symposium on Software Testing and Analysis. 605–616.                 Junda Zhang, Jiahao Li, Yunxin Li, Shijue Huang, et al. 2025. Ui-tars: Pioneering
     doi:10.1145/3533767.3534402                                                                automated gui interaction with native agents. arXiv preprint arXiv:2501.12326
[19] Yongxiang Hu, Hailiang Jin, Xuan Wang, Jiazhen Gu, Shiyu Guo, Chaoyi Chen,                 (2025).
     Xin Wang, and Yangfan Zhou. 2024. Autoconsis: Automatic gui-driven data               [41] Dezhi Ran, Hao Wang, Zihe Song, Mengzhou Wu, Yuan Cao, Ying Zhang, Wei
     inconsistency detection of mobile apps. In Proceedings of the 46th International           Yang, and Tao Xie. 2024. Guardian: A Runtime Framework for LLM-based UI
     Conference on Software Engineering: Software Engineering in Practice. 137–146.             Exploration. In Proceedings of the 33rd ACM SIGSOFT International Symposium
[20] John Hughes. 2016. Experiences with QuickCheck: testing the hard stuff and                 on Software Testing and Analysis.
     staying sane. In A List of Successes That Can Change the World: Essays Dedicated      [42] Oliviero Riganelli, Simone Paolo Mottadelli, Claudio Rota, Daniela Micucci, and
     to Philip Wadler on the Occasion of His 60th Birthday. Springer, 169–186.                  Leonardo Mariani. 2020. Data loss detector: automatically revealing data loss
[21] John Hughes, Benjamin C Pierce, Thomas Arts, and Ulf Norell. 2016. Mysteries               bugs in Android apps. In ISSTA ’20: 29th ACM SIGSOFT International Symposium
     of dropbox: property-based testing of a distributed synchronization service. In            on Software Testing and Analysis. 141–152. doi:10.1145/3395363.3397379
     2016 IEEE International Conference on Software Testing, Verification and Validation
     (ICST). IEEE, 135–145.
Conference’17, July 2017, Washington, DC, USA                                                                      Yiheng Xiong, Shiwen Song, Bo Ma, Ting Su, and Xiaofei Xie


[43] André Santos, Alcino Cunha, and Nuno Macedo. 2018. Property-based testing for         [65] Yiheng Xiong, Ting Su, Jingling Sun, Jue Wang, Qin Li, Geguang Pu, and Zhen-
     the robot operating system. In Proceedings of the 9th ACM SIGSOFT International            dong Su. 2026. From Natural Language to Executable Properties for Property-
     Workshop on Automating TEST Case Design, Selection, and Evaluation. 56–62.                 based Testing of Mobile Apps. arXiv:2603.21263 [cs.SE] https://arxiv.org/abs/
[44] Max Schäfer, Sarah Nadi, Aryaz Eghbali, and Frank Tip. 2023. An empirical                  2603.21263
     evaluation of using large language models for automated unit test generation.         [66] Yiheng Xiong, Ting Su, Jue Wang, Jingling Sun, Geguang Pu, and Zhendong
     IEEE Transactions on Software Engineering 50, 1 (2023), 85–105.                            Su. 2024. General and Practical Property-based Testing for Android Apps. In
[45] Koushik Sen, Darko Marinov, and Gul Agha. 2005. CUTE: A concolic unit testing              Proceedings of the 39th IEEE/ACM International Conference on Automated Software
     engine for C. ACM SIGSOFT software engineering notes 30, 5 (2005), 263–272.                Engineering. 53–64.
[46] Sina Shamshiri. 2015. Automated unit test generation for evolving software. In        [67] Yiheng Xiong, Mengqian Xu, Ting Su, Jingling Sun, Jue Wang, He Wen, Geguang
     Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering.         Pu, Jifeng He, and Zhendong Su. 2023. An empirical study of functional bugs in
     1038–1041.                                                                                 android apps. In Proceedings of the 32nd ACM SIGSOFT International Symposium
[47] Ting Su, Guozhu Meng, Yuting Chen, Ke Wu, Weiming Yang, Yao Yao, Geguang Pu,               on Software Testing and Analysis (ISSTA’23). 1319–1331.
     Yang Liu, and Zhendong Su. 2017. Guided, Stochastic Model-based GUI Testing           [68] Lin Yang, Chen Yang, Shutao Gao, Weijing Wang, Bo Wang, Qihao Zhu, Xiao Chu,
     of Android Apps. In The joint meeting of the European Software Engineering                 Jianyi Zhou, Guangtai Liang, Qianxiang Wang, et al. 2024. On the evaluation of
     Conference and the ACM SIGSOFT Symposium on the Foundations of Software                    large language models in unit test generation. In Proceedings of the 39th IEEE/ACM
     Engineering (ESEC/FSE). 245–256. doi:10.1145/3106237.3106298                               International Conference on Automated Software Engineering. 1607–1619.
[48] Ting Su, Yichen Yan, Jue Wang, Jingling Sun, Yiheng Xiong, Geguang Pu, Ke             [69] Juyeon Yoon, Robert Feldt, and Shin Yoo. 2024. Intent-driven mobile gui test-
     Wang, and Zhendong Su. 2021. Fully automated functional fuzzing of Android                 ing with autonomous large language model agents. In 2024 IEEE Conference on
     apps for detecting non-crashing logic bugs. Proc. ACM Program. Lang. 5, OOPSLA             Software Testing, Verification and Validation (ICST). IEEE, 129–139.
     (2021), 1–31. doi:10.1145/3485533                                                     [70] Zhiqiang Yuan, Mingwei Liu, Shiji Ding, Kaixin Wang, Yixuan Chen, Xin Peng,
[49] Jingling Sun, Ting Su, Jiayi Jiang, Jue Wang, Geguang Pu, and Zhendong Su. 2023.           and Yiling Lou. 2024. Evaluating and improving chatgpt for unit test generation.
     Property-Based Fuzzing for Finding Data Manipulation Errors in Android Apps.               Proceedings of the ACM on Software Engineering 1, FSE (2024), 1703–1726.
     In Proceedings of the 31st ACM Joint European Software Engineering Conference         [71] Razieh Nokhbeh Zaeem, Mukul R. Prasad, and Sarfraz Khurshid. 2014. Automated
     and Symposium on the Foundations of Software Engineering (ESEC/FSE). 1088–1100.            Generation of Oracles for Testing User-Interaction Features of Mobile Apps. In
     doi:10.1145/3611643.3616286                                                                Proceedings of the International Conference on Software Testing, Verification and
[50] Jingling Sun, Ting Su, Junxin Li, Zhen Dong, Geguang Pu, Tao Xie, and Zhendong             Validation (ICST). 183–192. doi:10.1109/ICST.2014.31
     Su. 2021. Understanding and finding system setting-related defects in Android         [72] Chi Zhang, Zhao Yang, Jiaxuan Liu, Yanda Li, Yucheng Han, Xin Chen, Zebiao
     apps. In ISSTA ’21: 30th ACM SIGSOFT International Symposium on Software                   Huang, Bin Fu, and Gang Yu. 2025. Appagent: Multimodal agents as smartphone
     Testing and Analysis. 204–215. doi:10.1145/3460319.3464806                                 users. In Proceedings of the 2025 CHI Conference on Human Factors in Computing
[51] Jingling Sun, Ting Su, Kai Liu, Chao Peng, Zhao Zhang, Geguang Pu, Tao Xie,                Systems. 1–20.
     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 deep-
     state 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 Con-
     ference 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).
