LIFT: Automating Symbolic Execution Optimization with Large Language Models for AI Networks

Chunchi Liu; Kaidi Xu; Kun Li; Minghui Xu; Ruoxi Wang; Xiuzhen Cheng; Yinhao Xiao; Yue Zhang

REVIEW 4 major objections 7 minor 23 references

LIFT: Automating Symbolic Execution Optimization with Large Language Models for AI Networks

T0 review · 4 major / 7 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read LIFT claims that an LLM-based pipeline can automatically rewrite the intermediate representation of a program so that dynamic symbolic execution runs faster, with a 53.5% runtime reduction on one binary, while the rewritten code stays…

desk verdict A plausible LLM-based IR simplification pipeline whose speedup claims are testable, but whose functional-correctness claim rests on an informal diff and is unsupported as written. read the letter →

arxiv 2507.04931 v1 pith:BOKP2F7R submitted 2025-07-07 cs.CR

Ruoxi Wang , Kun Li , Minghui Xu , Yue Zhang , Kaidi Xu , Chunchi Liu , Yinhao Xiao , Xiuzhen Cheng This is my paper · ORCID

classification cs.CR

keywords dynamicsymbolicexecutionintermediaterepresentationVEXIRlargelanguagemodelsbinaryanalysisoptimizationsemanticequivalenceLLM-assistedprogramtransformation

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper tries to establish that large language models can replace hand-written rules for optimizing the intermediate representation (IR) used in dynamic symbolic execution. It presents LIFT, a two-phase pipeline that profiles basic blocks of the IR, asks an LLM to rewrite the most time-consuming statements into simpler but semantically equivalent ones, and then validates the rewrites by benchmarking and component-level semantic comparison. The reported experiments on ten real-world binaries show consistent reductions in execution time and IR complexity, including a 53.5% reduction on bigtest and a 10.24% reduction on random. If the claim holds, symbolic execution of complex and networked binaries becomes more scalable without changing program behavior.

What carries the argument

The central mechanism is a two-phase, context-aware rewrite loop. First, the IR from a binary is split into basic blocks, each block's execution cost is measured under instrumentation, and the most expensive blocks are selected. Second, individual statements from those blocks are given to an LLM with a prompt asking for a functionally equivalent, shorter version; the outputs are filtered for syntax, reinserted into the IR, and then scored by a symbolic cost model. The kept rewrites are benchmarked for runtime and path coverage and verified by a component-level comparison of the original and transformed IR, so that control flow is never altered and only statement-level simplifications survive.

What would settle it

Pick one rewritten block from the paper's bigtest case, encode the original and transformed VEX statements as SMT formulas with symbolic inputs, and ask the solver for an input on which the two exit states differ; a satisfiable difference would refute the claim that semantic correctness is preserved by the pipeline.

Watch

Extended reading notes

Core claim

The discovery the paper defends is that statement-level IR rewriting by an LLM is a viable and generalizable optimization for symbolic execution. Given a time-intensive basic block, LIFT converts each costly statement into a simpler VEX IR statement, preserves control flow, and only keeps rewrites that pass a semantic verification step comparing variables, memory addresses, constants, and structure. The paper reports that across all ten benchmark programs every metric improved: execution time fell in every case, IR statement counts dropped by 90 to 222, and temporary-variable usage fell sharply in several binaries. Correctness is claimed through the verification step, which the paper describes as trading some precision for scalability.

Load-bearing premise

The load-bearing assumption is that the component-level semantic comparison, which the paper admits has a slight precision trade-off, is enough to guarantee that every rewritten IR block does exactly what the original block does.

Editorial extensions

If this is right

IR optimization in symbolic-execution tools can be automated by prompting an LLM instead of hand-authoring transformation rules.
Runtime gains concentrate in binaries with heavy symbolic arithmetic and memory operations, so profiling-based selection is the right first step.
The semantic verification step makes the pipeline applicable to unfamiliar binaries, since it checks each rewrite before accepting it.
Statement-level rewrites are safe enough to apply across many basic blocks, but block-level and control-flow-level optimizations are left for future work.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Editorial extension: applying the same profile-and-rewrite loop to other IR families, such as LLVM IR or GIMPLE, is a direct testable extension because the paper's mechanism does not depend on VEX-specific details.
Editorial extension: because the verification is component-level and LLM-assisted, the correctness guarantee is probabilistic rather than formal; a stronger claim would require an SMT-based equivalence check on each rewritten block.
Editorial extension: the symbolic cost model could be combined with superoptimization or equality-saturation techniques to discover simpler statements that an LLM alone might miss.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The paper's core idea—use an LLM to rewrite VEX IR statements inside angr's symbolic execution pipeline, guided by a profiling-based selection—is genuinely new and worth a look. The 53.5% speedup on bigtest is eye-catching, and the consistent structural reductions (fewer IR statements, PUTs, temporaries) are objectively countable. The authors are also honest: they flag the precision trade-off in semantic verification and point to an anonymized repo. That's more than many papers do.

Where it falls down is the correctness half of the claim. The title says "functional-equivalent IR transformation," but the verification in Section 3.2(II) compares original and transformed IR at the component level using a DeepDiff-style structural comparison with LLM assistance. The paper itself admits "a slight trade-off in precision." Structural similarity is neither necessary nor sufficient for semantic equivalence, and no definition of the equivalence relation is given. So every assertion that semantics were preserved—including the blanket statement in Section 4.2 that "semantic correctness was maintained in all optimized programs"—is traced back to a check that is not up to the job. The stress-test note lands here. Without an independent equivalence check (or at least a detailed, quantified characterization of the verifier's errors), the central claim is only half-supported.

The evaluation is also thinner than the abstract suggests. Ten binaries is a small set, and none of them look like real distributed AI network workloads despite the title and framing. Most improvements are 1–5%; the 53.5% is a single uncontextualized number. No error bars, significance tests, or repeated-seed variance are reported, even though runtime is averaged over 100 runs. There is no baseline comparison to manual IR rewriting or a conventional optimizer, so we don't know whether an LLM is adding value over simpler rule-based approaches. The symbolic cost model is self-defined and unquantified, which introduces selection bias, though not circularity—the runtime measurements are external to the LLM's choices, and the structural metrics are directly countable.

What holds up: the speedup measurements are against angr's real runtime, independent of LLM internals, so the speedup half is not circular. The structural simplifications are real reductions in IR complexity, even if their causal link to the speedup isn't analyzed. The paper deserves a serious referee, but it should come back with major revisions: either formalize the equivalence check or replace it with an actual symbolic equivalence validator, add statistical rigor, and test on realistic workloads that match the AI-networks framing. For now, I'd treat this as a promising Systems-style idea in need of a much stronger correctness argument, not as a finished result.

Referee Report

4 major / 7 minor

Summary. The paper presents LIFT, a framework that uses large language models (GPT-4o) to optimize VEX intermediate representation (IR) statements in the angr symbolic execution engine. The framework extracts time-intensive IR blocks, profiles their cost, and uses an LLM to rewrite individual statements into shorter or simpler equivalents. The rewritten IR is then benchmarked for execution-time and structural improvements, and a semantic verification step compares original and transformed IR. Experiments on ten binaries report execution-time reductions between 0.75% and 53.5%, along with reductions in IR statement counts, PUT instructions, and temporary variables. The paper claims that all optimizations preserve functional correctness.

Significance. If the central claims are accepted, LIFT demonstrates a novel application of LLMs to low-level IR optimization in dynamic symbolic execution, with potential scalability advantages over manual rule-based rewriting. The evaluation is grounded in external runtime measurements against angr, which avoids circularity in the speedup assessment, and the code is made available in an anonymous repository. However, the correctness claim is not backed by a formal equivalence check, and the statistical support for the speedup results is thin. The connection to 'AI networks' is asserted but not directly evidenced by the benchmark selection. With strengthened verification and statistical reporting, the work could be a useful contribution to the symbolic execution and LLM-for-code communities.

major comments (4)

[Section 3.2(II), Section 5] The semantic verification step is described as comparing original and transformed IR 'at the component level' with variables, memory addresses, constants, and overall structure, assisted by LLMs, and the Discussion explicitly acknowledges 'a slight trade-off in precision compared to manual methods.' This structural comparison is neither necessary nor sufficient for semantic equivalence of VEX IR: two blocks can be semantically equal while differing in temporary allocation or statement partitioning, and semantically different while looking structurally similar (e.g., a change in overflow behavior or flag-setting). The paper never defines the equivalence relation, never states whether the comparison is syntactic or semantic, and never quantifies the precision loss. Because the claims that 'semantic correctness was maintained in all optimized programs' (Section 4.2) and that 'all optimizations preserved original behavior' (Section 5) depend entirely on this step, the correctness half of the central claim is unsupported as written. The authors should either replace this step with an independent semantic equivalence check (e.g., differential symbolic execution or SMT-based equivalence of original and transformed blocks) or downgrade the claims to structural verification and discuss the residual risk.
[Section 4.2, Table 1] The speedup results are reported as single percentage improvements with no variance, confidence intervals, or significance tests. Although Section 4.1 states that execution time is the average over 100 symbolic runs per binary, Table 1 provides only the percentage change, and Table 2 gives absolute times for bigtest alone. Without per-binary standard deviations or a paired significance test, the reader cannot determine whether improvements as small as 0.75% (bigprog) or 1.02% (matrix) are distinguishable from run-to-run noise. The 53.5% improvement for bigtest is striking but presented as a single uncontextualized measurement. The paper should report the full distribution of the 100 runs (e.g., mean ± std, box plots) and apply a paired statistical test (e.g., Wilcoxon signed-rank or paired t-test) across runs to support the 'consistent performance improvements' claim.
[Section 3.2(I)] The symbolic cost model used to select statements for transformation is described only qualitatively: 'statements that involve complex arithmetic operations, memory stores, or symbolic variable assignments are assigned higher weights.' Neither the weights nor the 'top-ranking statements' threshold are specified, so the selection procedure is not reproducible and the potential selection bias is unquantified. Because the reported results depend on which statements are chosen for LLM rewriting, the authors must provide the exact cost weights, the number of statements selected per binary, and the selection criterion (e.g., top-k by cost). Without these details, a reader cannot assess whether the improvements are due to the LLM or to the particular selection heuristic, and the method cannot be independently reimplemented.
[Section 4.1] The dataset section describes the ten binaries at a high level (e.g., 'counter and matrix represent lightweight tasks... require efficient data transfers and synchronization') but provides no concrete details about their provenance, source language, compilation flags, target architecture, or input workloads. As a result, the reader cannot judge whether these are representative of real-world AI network binaries or toy programs, and the paper's framing 'for AI Networks' is not evidenced. The authors should include a table with binary names, descriptions, sizes (e.g., number of IR blocks or instructions), and justification of relevance to networked AI systems. This is needed for the external validity of the evaluation and for the claimed scope of the method.

minor comments (7)

[Figure 2] The VEX IR example is garbled: 't1 = (t0, x30)' should show the operation (e.g., 't1 = Sub64(t0, 0x30)'), and the optimized PUT line is unreadable. Please fix the notation and rendering.
[Section 2.1] The sentence 'In distributed AI systems, where network protocols and communication patterns play a significant role.' is a fragment; it should be completed or integrated with the preceding sentence.
[Section 2.1, Reference [9]] Reference [9] (Merckx et al., 'Equality Saturation for Optimizing High-Level Julia IR') is cited as a 'newer hybrid fuzzing framework like SymFusion'; this appears to be a citation mismatch. Please correct the reference or the description.
[Section 3.2(I)] The sentence 'for semantically similar blocks, if we can identify the simplest equivalent, we can reuse that simplified version across multiple instances' suggests a cross-block reuse mechanism that is not described in Section 3.1(II) or evaluated. Either implement and evaluate this reuse or remove the claim.
[Section 4.2, Table 1] The column heading 'Memory Instructions' in Table 1 is inconsistent with 'PUT Instruction Count' in Table 2 and with the criteria in Section 4.1 ('Memory Instructions: Count the number of operations'). Please standardize the terminology across the paper.
[Section 4.1] The paper does not report the LLM inference cost or the total wall-clock time of the optimization phase. Since the paper advocates LLM-based optimization, the overhead should be quantified to assess the practical trade-off between optimization time and symbolic execution speedup.
[Section 4] The evaluation lacks a baseline comparison (e.g., random statement selection, rule-based simplification, or angr's own IR simplification passes). Adding such a baseline would help isolate the contribution of the LLM and support the claim that LLM-based rewriting is beneficial.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity: measured speedups are independent of the LLM's choices, though the informal LLM-assisted semantic verification leaves correctness under-supported.

full rationale

LIFT's performance claims are not circular: the execution-time, IR-statement, PUT-instruction, and temporary-variable reductions are measured by re-running angr on the rewritten IR and comparing against the original runs (Section 4.1 Methodology; Section 4.2, Tables 1-2). No fitted parameter is reused as the predicted outcome; the LLM is prompted to simplify statements and the resulting binaries are benchmarked externally, so the speedup result is not forced by construction. The genuinely weak load-bearing step is the correctness half of the central claim, which rests on Section 3.2(II)'s Semantic Verification: an LLM-assisted component-level comparison that explicitly accepts 'a slight trade-off in precision compared to manual methods.' This is an informal and potentially self-referential check, and the paper never formalizes the equivalence relation or quantifies its precision loss. However, that weakness is an under-verified correctness claim, not a circular reduction: nothing in the paper makes the verification output identical to the input by construction, and there is no fitted parameter renamed as a prediction. The self-citations that motivate the problem, e.g., [21] on compiler optimizations degrading symbolic execution, are relevant but not load-bearing because the present results are independently measured. Overall, no significant circularity is present.

Assumptions & free parameters 2 free parameters · 3 assumptions · 0 invented entities

The central claims rest on an unquantified cost model, a non-formal verification step, and an implicit reliance on angr's IR correctness.

free parameters (2)

symbolic cost model weights = not specified
The cost model assigning weights to instruction types (complex arithmetic, memory stores, symbolic assignments) is used to select high-cost statements for optimization. Values are not given in the paper.
top-statement selection threshold = not specified
The number of top-ranking statements selected for transformation per block is not reported.

assumptions (3)

domain assumption angr's VEX IR faithfully represents the semantics of x86 binaries
The entire optimization operates on VEX IR extracted by angr; if the IR is incorrect, optimizations and verification are meaningless. See Section 3.1.
domain assumption Structured component-level comparison (DeepDiff) detects all semantic changes
Semantic verification relies on comparing variables, addresses, constants, and structure; the paper admits LLM assistance trades off precision. See Section 3.2(II).
ad hoc to paper LLM output is syntactically valid after filtering
The pipeline filters and cleans LLM output; the paper does not quantify failure rates. See Section 3.1(II).

how reviews work

0 comments

Cite this review

Pith. "Pith review of LIFT: Automating Symbolic Execution Optimization with Large Language Models for AI Networks." pith.science (2026). https://pith.science/paper/BOKP2F7R

@misc{pith2026250704931,
  author       = {Pith},
  title        = {Pith review of: LIFT: Automating Symbolic Execution Optimization with Large Language Models for AI Networks},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BOKP2F7R}},
  note         = {Machine review of arXiv:2507.04931}
}

read the original abstract

Dynamic Symbolic Execution (DSE) is a key technique in program analysis, widely used in software testing, vulnerability discovery, and formal verification. In distributed AI systems, DSE plays a crucial role in identifying hard-to-detect bugs, especially those arising from complex network communication patterns. However, traditional approaches to symbolic execution are often hindered by scalability issues and inefficiencies, particularly in large-scale systems. This paper introduces LIFT (Large-language-model Integrated Functional-equivalent-IR Transformation), a novel framework that leverages Large Language Models (LLMs) to automate the optimization of Intermediate Representations (IRs) in symbolic execution. LIFT addresses the challenges of symbolic execution by providing a scalable, context-sensitive solution for IR transformation. The framework consists of two phases: IR Analysis and Optimization, where LLMs optimize time-intensive IR blocks, and Symbolic Execution and Validation, which includes benchmarking and semantic verification to ensure correctness and generalizability. Experiments on real-world binaries demonstrated significant performance improvements, including a 53.5\% reduction in execution time for bigtest and a 10.24\% reduction for random, along with reductions in IR statements, PUT instructions, and temporary variables. These results demonstrate that LLMs simplify IRs while maintaining functional correctness, enhancing symbolic execution in distributed AI systems.

Figures

Figures reproduced from arXiv: 2507.04931 by the authors.

**Figure 1.** The architecture of LIFT recent work by Luo et al.[8] leveraged SMT solver time prediction to reduce the overhead associated with expensive constraints, thereby improving the symbolic execution process under strict time budgets. While these approaches optimize the symbolic execution workflow in terms of search and constraint-solving, they do not directly address the cost and efficiency of the IR used for analyzin… view at source ↗

**Figure 2.** An example of LLM optimization of VEX IR [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

23 extracted references · 15 canonical work pages

[1]

S. Cha, S. Hong, J. Bak, J. Kim, J. Lee, and H. Oh. 2022. Enhancing Dy- namic Symbolic Execution by Automatically Learning Search Heuris- tics. In IEEE Trans. Software Engineering , Vol. 48. IEEE, 3640–3663. https://doi.org/10.1109/TSE.2020.3029878

work page arXiv 2022
[2]

Ye Cheng, Minghui Xu, Yue Zhang, Kun Li, Ruoxi Wang, and Lian Yang. 2024. AutoIoT: Automated IoT Platform Using Large Language Models. IEEE Internet of Things Journal (2024)

work page 2024
[3]

Ye Cheng, Minghui Xu, Yue Zhang, Kun Li, Hao Wu, Yechao Zhang, Shaoyong Guo, Wangjie Qiu, Dongxiao Yu, and Xiuzhen Cheng. 2025. Say What You Mean: Natural Language Access Control with Large Lan- guage Models for Internet of Things. arXiv preprint arXiv:2505.23835 (2025)

arXiv 2025
[4]

Dutta, R

A. Dutta, R. Maghareh, and J. Jaffar. 2020. TracerX: Pruning Dynamic Symbolic Execution with Weakest Precondition Interpolation. In Proc. 2020 International Symposium on Software Testing and Analysis (ISSTA). 112–122. https://doi.org/10.1145/3395363.3397355

arXiv 2020
[5]

Huang, X

K. Huang, X. Meng, J. Zhang, Y. Liu, W. Wang, S. Li, and Y. Zhang

work page
[6]

Yue Li, Xiao Li, Hao Wu, Yue Zhang, Xiuzhen Cheng, Sheng Zhong, and Fengyuan Xu. 2024. Attention is all you need for llm-based code vulnerability localization. arXiv preprint arXiv:2410.15288 (2024)

arXiv 2024
[7]

Z. Li, S. Dutta, and M. Naik. 2025. IRIS: LLM-Assisted Static Analysis for Detecting Security Vulnerabilities. In Proc. Int. Conf. on Learning Representations (ICLR) . Online. Available: https://openreview.net/forum?id=your-id

work page 2025
[8]

S. Luo, H. Xu, Y. Bi, X. Wang, and Y. Zhou. 2021. Boosting Symbolic Execution via Constraint Solving Time Prediction (Experience Paper). In Proc. 30th ACM SIGSOFT Int. Symp. on Software Testing and Analysis (ISSTA). 239–251. https://doi.org/10.1145/3460319.3464825

arXiv 2021

Show all 23 references

[9]

Merckx, T

J. Merckx, T. Besard, and B. De Sutter. 2025. Equality Saturation for Optimizing High-Level Julia IR. In Proc. 2025 ACM SIGSAC Conference on Computer and Communications Security (CCS)

2025
[10]

Nethercote and J

N. Nethercote and J. Seward. 2007. Valgrind: A Framework for Heavy- weight Dynamic Binary Instrumentation. In Proc. ACM SIGPLAN 2007 Conf. on Programming Language Design and Implementation (PLDI) . 89–100

2007
[11]

Pitigalaarachchi, X

P. Pitigalaarachchi, X. Ding, H. Qiu, H. Tu, J. Hong, and L. Jiang. 2023. KRover: A Symbolic Execution Engine for Dynamic Kernel Analysis. In Proc. 2023 ACM SIGSAC Conf. on Computer and Communications Security (CCS). Copenhagen, Denmark, 2009–2023

2023
[12]

Poeplau and A

S. Poeplau and A. Francillon. 2020. Symbolic Execution with SYMCC: Don’t Interpret, Compile!. In Proc. 29th USENIX Security Symposium (USENIX Security). 181–198

2020
[13]

Shoshitaishvili, R

Y. Shoshitaishvili, R. Wang, C. Salls, N. Stephens, M. Polino, A. Dutcher, J. Grosen, S. Feng, C. Hauser, C. Kruegel, and G. Vigna. 2016. (State of) The Art of War: Offensive Techniques in Binary Analysis. In Proc. IEEE Symposium on Security and Privacy (S&P) . 138–157. https:...

2016 doi
[14]

JaeSeung Song, Cristian Cadar, and Peter Pietzuch. 2014. SymbexNet: Testing network protocol implementations with symbolic execution and rule-based specifications. IEEE Transactions on Software Engineer- ing 40, 7 (2014), 695–709

2014
[15]

Radu Stoenescu, Matei Popovici, Lorina Negreanu, and Costin Raiciu
[16]

H. Tu, L. Jiang, X. Ding, and H. Jiang. 2022. FastKLEE: Faster Symbolic Execution via Reducing Redundant Bound Checking of Type-Safe Pointers. In Proc. ACM Joint European Software Engineering Conf. and Symp. on the Foundations of Software Engineering (ESEC/FSE) . 49–59. https:...

2022
[17]

C. S. Xia, M. Paltenghi, J. L. Tian, M. Pradel, and L. Zhang. 2024. Fuzz4All: Universal Fuzzing with Large Language Models. InProc. 46th IEEE/ACM Int. Conf. on Software Engineering (ICSE) . Lisbon, Portugal, 1–13. https://doi.org/10.1145/3597503.3639121

2024
[18]

Biwei Yan, Kun Li, Minghui Xu, Yueyan Dong, Yue Zhang, Zhaochun Ren, and Xiuzhen Cheng. 2024. On protecting the data privacy of large language models (llms): A survey.arXiv preprint arXiv:2403.05156 (2024)

2024 arXiv
[19]

Biwei Yan, Kun Li, Minghui Xu, Yueyan Dong, Yue Zhang, Zhaochun Ren, and Xiuzhen Cheng. 2025. On protecting the data privacy of Large Language Models (LLMs) and LLM agents: A literature review. High-Confidence Computing (2025), 100300

2025
[20]

Yifan Yao, Jinhao Duan, Kaidi Xu, Yuanfang Cai, Zhibo Sun, and Yue Zhang. 2024. A survey on large language model (llm) security and privacy: The good, the bad, and the ugly. High-Confidence Computing (2024), 100211

2024
[21]

Zhang, M

Y. Zhang, M. Sirlanci, R. Wang, and Z. Lin. 2024. When Compiler Optimizations Meet Symbolic Execution: An Empirical Study. In Proc. 2024 ACM SIGSAC Conf. on Computer and Communications Security (CCS). 4212–4225. https://doi.org/10.1145/3618257.3632166 7

2024
[2016]

In Proceedings of the 2016 ACM SIGCOMM Conference

Symnet: Scalable symbolic execution for modern networks. In Proceedings of the 2016 ACM SIGCOMM Conference . 314–327

2016
[2023]

An Empirical Study on Fine-Tuning Large Language Models of Code for Automated Program Repair. In Proc. 38th IEEE/ACM Int. Conf. on Automated Software Engineering (ASE) . Luxembourg City, Luxembourg, 612–623

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.

[1] [1]

S. Cha, S. Hong, J. Bak, J. Kim, J. Lee, and H. Oh. 2022. Enhancing Dy- namic Symbolic Execution by Automatically Learning Search Heuris- tics. In IEEE Trans. Software Engineering , Vol. 48. IEEE, 3640–3663. https://doi.org/10.1109/TSE.2020.3029878

work page arXiv 2022

[2] [2]

Ye Cheng, Minghui Xu, Yue Zhang, Kun Li, Ruoxi Wang, and Lian Yang. 2024. AutoIoT: Automated IoT Platform Using Large Language Models. IEEE Internet of Things Journal (2024)

work page 2024

[3] [3]

Ye Cheng, Minghui Xu, Yue Zhang, Kun Li, Hao Wu, Yechao Zhang, Shaoyong Guo, Wangjie Qiu, Dongxiao Yu, and Xiuzhen Cheng. 2025. Say What You Mean: Natural Language Access Control with Large Lan- guage Models for Internet of Things. arXiv preprint arXiv:2505.23835 (2025)

arXiv 2025

[4] [4]

Dutta, R

A. Dutta, R. Maghareh, and J. Jaffar. 2020. TracerX: Pruning Dynamic Symbolic Execution with Weakest Precondition Interpolation. In Proc. 2020 International Symposium on Software Testing and Analysis (ISSTA). 112–122. https://doi.org/10.1145/3395363.3397355

arXiv 2020

[5] [5]

Huang, X

K. Huang, X. Meng, J. Zhang, Y. Liu, W. Wang, S. Li, and Y. Zhang

work page

[6] [6]

Yue Li, Xiao Li, Hao Wu, Yue Zhang, Xiuzhen Cheng, Sheng Zhong, and Fengyuan Xu. 2024. Attention is all you need for llm-based code vulnerability localization. arXiv preprint arXiv:2410.15288 (2024)

arXiv 2024

[7] [7]

Z. Li, S. Dutta, and M. Naik. 2025. IRIS: LLM-Assisted Static Analysis for Detecting Security Vulnerabilities. In Proc. Int. Conf. on Learning Representations (ICLR) . Online. Available: https://openreview.net/forum?id=your-id

work page 2025

[8] [8]

S. Luo, H. Xu, Y. Bi, X. Wang, and Y. Zhou. 2021. Boosting Symbolic Execution via Constraint Solving Time Prediction (Experience Paper). In Proc. 30th ACM SIGSOFT Int. Symp. on Software Testing and Analysis (ISSTA). 239–251. https://doi.org/10.1145/3460319.3464825

arXiv 2021