pith. sign in

arxiv: 2606.10264 · v1 · pith:VWJAANGAnew · submitted 2026-06-09 · 💻 cs.CR · cs.SE

RECON: An LLM-Enhanced Backward Constraint Analysis Framework

Babangida Bappah , Lamine Noureddine , Umar Farooq , Aisha Ali-Gombe This is my paper

Pith reviewed 2026-06-27 13:11 UTC · model grok-4.3

classification 💻 cs.CR cs.SE
keywords constraint analysisAndroid bytecodeLLMsymbolic executionbackward analysismalware analysisprogram analysissemantic specifications
0
0 comments X

The pith

RECON combines static analysis with large language models to extract precise constraints from Android bytecode faster than symbolic execution.

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

The paper introduces RECON as a framework that starts from target methods in Android apps and works backward to entry points while using LLMs to turn low-level bytecode conditions into readable specifications. Traditional symbolic execution struggles with path explosion and loss of meaning in complex Android environments that involve heavy framework calls and event handling. By adding LLM reasoning on top of backward path discovery, the approach seeks to keep the precision of static analysis while gaining semantic clarity and speed. Evaluation across 78 scenarios shows it runs 5.8 times faster with full success and logical equivalence to symbolic methods, plus more usable output. On 100 malware samples it reaches 84 percent success at surfacing constraints tied to dangerous API calls.

Core claim

RECON performs backward path discovery from target method(s) to the application entry point(s), discovers method-level control-flow constraints, and leverages LLM reasoning to transform bytecode conditions into interpretable specifications. Results demonstrate that the approach operates 5.8X faster than traditional symbolic execution, with a 100% success rate, while maintaining logical equivalence and providing significantly more precise and interpretable output. On 100 malware samples the framework reaches an 84% success rate in generating semantic constraints that lead to dangerous API behaviors and in detecting complex constraints across multiple execution paths.

What carries the argument

Backward path discovery from target methods combined with LLM transformation of bytecode conditions into interpretable semantic specifications.

If this is right

  • The method maintains logical equivalence to symbolic execution while running 5.8 times faster across the tested scenarios.
  • Output is more precise and directly interpretable than traditional symbolic results.
  • On malware samples the framework identifies semantic constraints for dangerous API behaviors in 84 percent of cases.
  • Complex constraints spanning multiple execution paths are detected at the reported success rate.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same backward-plus-LLM pattern could be applied to other bytecode or intermediate representations that lose high-level intent.
  • Interpretable specifications produced by the system might serve as input for further automated checks or human review in security workflows.
  • Performance on the 78 scenarios and 100 samples leaves open whether the speed and accuracy hold when the number of paths or framework depth increases substantially.

Load-bearing premise

Large language models can reliably turn low-level bytecode conditions into accurate and complete semantic specifications without errors even when Android framework interactions and event-driven code are present.

What would settle it

A program where the LLM-derived specification produces a constraint that differs in logical meaning from the actual bytecode, leading to incorrect conclusions about which paths reach a target method.

Figures

Figures reproduced from arXiv: 2606.10264 by Aisha Ali-Gombe, Babangida Bappah, Lamine Noureddine, Umar Farooq.

Figure 1
Figure 1. Figure 1: RECON Framework workflow 3.1. Backward Path Discovery In backward path discovery, we identify interprocedural execution paths from target methods to application entry points through call graph traversal. Let T denote a target method within an Android application, and G = (V, E) denote the application’s call graph where V is the set of reachable methods and E represents caller-callee relation￾ships. To accu… view at source ↗
Figure 2
Figure 2. Figure 2: Let T denote the target callsite corresponding to the savePrice(String, float) invocation. During upward traversal of the method’s CF Gm, the first decision point encountered is the conditional [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 2
Figure 2. Figure 2: Jimple bytecode from onOptions() showing conditional statements and the target invocation, with decision points represented as D = ⟨d1, . . . , dn⟩. statement if z0 == 0gotolabel1 (line 10). The LLM receives this conditional node together with the complete method bytecode and the target method savePrice. By analyzing the surrounding control-flow structure, the LLM determines that taking the true branch tra… view at source ↗
Figure 3
Figure 3. Figure 3: LLM Performance Consistency Analysis. Box plot showing preci [PITH_FULL_IMAGE:figures/full_fig_p015_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: Malware location access execution path and constraint require [PITH_FULL_IMAGE:figures/full_fig_p015_5.png] view at source ↗
Figure 4
Figure 4. Figure 4: LLM prompt template for semantic constraint extraction using [PITH_FULL_IMAGE:figures/full_fig_p015_4.png] view at source ↗
read the original abstract

While traditional techniques, such as symbolic execution, provide a principled foundation for precise constraint reasoning in program analysis, they struggle to scale to modern software systems mainly due to path explosion, the need for function modeling, and the loss of semantic intent at low-level program representations. In complex execution environments such as Android, characterized by extensive framework interactions and event-driven behavior, these limitations are even more amplified. Thus, in this paper, we present a novel large language model (LLM)-enhanced backward constraint analysis framework that combines the precision of static program analysis with LLM's semantic understanding to extract precise execution constraints from Android bytecode. Our approach, titled RECON, performs backward path discovery from target method(s) to the application entry point(s), discovers method-level control-flow constraints, and leverages LLM reasoning to transform bytecode conditions into interpretable specifications. We evaluated RECON using five LLMs across 78 Android constraint-extraction scenarios and compared it with traditional symbolic execution on real-world applications. Results demonstrate that our approach operates 5.8X faster than traditional symbolic execution, with a 100% success rate, while maintaining logical equivalence and providing significantly more precise and interpretable output. We further evaluated RECON for malware analysis on 100 samples. The results indicate an 84% success rate in generating semantic constraints that lead to the execution of dangerous API behaviors and in detecting complex constraints across multiple execution paths.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper introduces RECON, a framework that augments backward constraint analysis for Android bytecode with LLM reasoning. It performs backward path discovery from target methods to entry points, extracts method-level control-flow constraints via static analysis, and uses LLMs to convert low-level bytecode conditions into interpretable semantic specifications. On 78 constraint-extraction scenarios the approach is reported to run 5.8X faster than symbolic execution while achieving 100% success and preserving logical equivalence; on 100 malware samples it achieves 84% success in producing constraints that expose dangerous API behaviors and complex multi-path constraints.

Significance. If the reported speedups and equivalence claims can be substantiated with explicit verification procedures, the work would offer a practical way to scale constraint reasoning to event-driven Android applications while producing human-interpretable output that pure symbolic methods typically lack. The combination of static-analysis precision with LLM semantic lifting addresses a recognized pain point in mobile security analysis.

major comments (2)
  1. [Abstract] Abstract: the central performance claim (5.8X faster than symbolic execution, 100% success rate, logical equivalence) is stated without any description of the baseline symbolic-execution implementation, the exact timing methodology, the set of 78 scenarios, or the concrete procedure used to establish logical equivalence between LLM-generated specifications and the original bytecode conditions. Because equivalence is required to support both the correctness and the speedup assertions, this omission is load-bearing.
  2. [Abstract] Abstract (malware evaluation paragraph): the 84% success rate on 100 samples is reported without defining the success criterion, the dangerous APIs considered, how multi-path constraints were enumerated, or any failure-case analysis. These details are necessary to assess whether the result supports the claim that RECON reliably surfaces dangerous behaviors.
minor comments (1)
  1. [Abstract] The abstract mentions evaluation with five LLMs but does not name them or indicate whether results were aggregated or reported per model; adding this information would improve reproducibility.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback highlighting the need for greater self-containment in the abstract. We will revise the abstract to incorporate concise descriptions of the evaluation methodology and success criteria, with references to the detailed sections in the body. Below we respond point by point to the major comments.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central performance claim (5.8X faster than symbolic execution, 100% success rate, logical equivalence) is stated without any description of the baseline symbolic-execution implementation, the exact timing methodology, the set of 78 scenarios, or the concrete procedure used to establish logical equivalence between LLM-generated specifications and the original bytecode conditions. Because equivalence is required to support both the correctness and the speedup assertions, this omission is load-bearing.

    Authors: The full manuscript (Section 4) describes the 78 scenarios, the symbolic-execution baseline, the wall-clock timing methodology on the evaluation hardware, and the logical-equivalence procedure (combining automated checks and expert review). We agree the abstract should be more self-contained on these points. We will revise the abstract to add a brief summary of the baseline and verification approach together with pointers to Section 4. revision: yes

  2. Referee: [Abstract] Abstract (malware evaluation paragraph): the 84% success rate on 100 samples is reported without defining the success criterion, the dangerous APIs considered, how multi-path constraints were enumerated, or any failure-case analysis. These details are necessary to assess whether the result supports the claim that RECON reliably surfaces dangerous behaviors.

    Authors: Section 5 defines success as the production of constraints that expose at least one dangerous API behavior and that capture complex multi-path constraints; it also enumerates the APIs and provides failure-case discussion. We will revise the abstract paragraph to include a concise statement of the success criterion and multi-path enumeration approach, again with a reference to Section 5. revision: yes

Circularity Check

0 steps flagged

No circularity: empirical framework evaluation with no self-referential derivations

full rationale

The paper describes an engineering framework (RECON) that chains existing backward static analysis steps with LLM calls for transforming bytecode conditions into specifications. No equations, fitted parameters, or mathematical derivations appear in the provided text. Performance claims (5.8X speedup, 100% success rate, logical equivalence) and malware-analysis results (84% on 100 samples) are presented as outcomes of external evaluations on 78 scenarios and 100 samples rather than quantities that reduce to the inputs by construction. Self-citations are absent from the abstract and evaluation summary. The central claims rest on reported experimental outcomes against external benchmarks, satisfying the self-contained criterion.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Only the abstract is available, so the ledger reflects high-level claims rather than detailed derivations. The central premise is the reliability of LLM semantic interpretation.

axioms (1)
  • domain assumption Large language models can accurately interpret and translate low-level bytecode conditions into high-level interpretable specifications
    This is the key step that allows the framework to overcome limitations of pure static analysis.

pith-pipeline@v0.9.1-grok · 5789 in / 1297 out tokens · 26838 ms · 2026-06-27T13:11:31.921149+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

69 extracted references · 2 canonical work pages · 1 internal anchor

  1. [1]

    Few-shot training llms for project-specific code-summarization

    Toufique Ahmed and Premkumar Devanbu. Few-shot training llms for project-specific code-summarization. InProceedings of the 37th IEEE/ACM international conference on automated software engineer- ing, pages 1–5, 2022

    2022

  2. [2]

    Automatic semantic augmentation of language model prompts (for code summarization)

    Toufique Ahmed, Kunal Suresh Pai, Premkumar Devanbu, and Earl Barr. Automatic semantic augmentation of language model prompts (for code summarization). InProceedings of the IEEE/ACM 46th international conference on software engineering, pages 1–13, 2024

    2024

  3. [3]

    Computational verification of c protocol implementations by symbolic execution

    Mihhail Aizatulin, Andrew D Gordon, and Jan J ¨urjens. Computational verification of c protocol implementations by symbolic execution. InProceedings of the 2012 ACM conference on Computer and communications security, pages 712–723, 2012

    2012

  4. [4]

    Androzoo: Collecting millions of android apps for the research community

    Kevin Allix, Tegawend ´e F Bissyand ´e, Jacques Klein, and Yves Le Traon. Androzoo: Collecting millions of android apps for the research community. InProceedings of the 13th international con- ference on mining software repositories, pages 468–471, 2016

    2016

  5. [5]

    Jpf–se: A symbolic execution extension to java pathfinder

    Saswat Anand, Corina S P ˘as˘areanu, and Willem Visser. Jpf–se: A symbolic execution extension to java pathfinder. InInternational conference on tools and algorithms for the construction and analysis of systems, pages 134–138. Springer, 2007

    2007

  6. [6]

    Flowdroid: Precise context, flow, field, object- sensitive and lifecycle-aware taint analysis for android apps.ACM sigplan notices, 49(6):259–269, 2014

    Steven Arzt, Siegfried Rasthofer, Christian Fritz, Eric Bodden, Alexandre Bartel, Jacques Klein, Yves Le Traon, Damien Octeau, and Patrick McDaniel. Flowdroid: Precise context, flow, field, object- sensitive and lifecycle-aware taint analysis for android apps.ACM sigplan notices, 49(6):259–269, 2014

    2014

  7. [7]

    Static analysis as a feedback loop: Enhancing llm-generated code beyond correctness

    Scott Blyth, Sherlock A Licorish, Christoph Treude, and Markus Wagner. Static analysis as a feedback loop: Enhancing llm-generated code beyond correctness. In2025 IEEE International Conference on Source Code Analysis & Manipulation (SCAM), pages 100–109. IEEE, 2025

    2025

  8. [8]

    Iterative distribution-aware sampling for probabilistic symbolic execution

    Mateus Borges, Antonio Filieri, Marcelo d’Amorim, and Corina S P˘as˘areanu. Iterative distribution-aware sampling for probabilistic symbolic execution. InProceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pages 866–877, 2015

    2015

  9. [9]

    Constraint normalization and parameterized caching for quantitative program analysis

    Tegan Brennan, Nestan Tsiskaridze, Nicol ´as Rosner, Abdulbaki Ay- din, and Tevfik Bultan. Constraint normalization and parameterized caching for quantitative program analysis. InProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, pages 535–546, 2017

    2017

  10. [10]

    Machine learning steered symbolic execution framework for complex software code.Formal Aspects of Computing, 33(3):301–323, 2021

    Lei Bu, Yongjuan Liang, Zhunyi Xie, Hong Qian, Yi-Qi Hu, Yang Yu, Xin Chen, and Xuandong Li. Machine learning steered symbolic execution framework for complex software code.Formal Aspects of Computing, 33(3):301–323, 2021

    2021

  11. [11]

    Sym- bolic execution for software testing in practice: preliminary assess- ment

    Cristian Cadar, Patrice Godefroid, Sarfraz Khurshid, Corina S P˘as˘areanu, Koushik Sen, Nikolai Tillmann, and Willem Visser. Sym- bolic execution for software testing in practice: preliminary assess- ment. InProceedings of the 33rd International Conference on Software Engineering, pages 1066–1071, 2011

    2011

  12. [12]

    Klee symbolic execution engine in 2019.International Journal on Software Tools for Technology Transfer, 23(6):867–870, 2021

    Cristian Cadar and Martin Nowack. Klee symbolic execution engine in 2019.International Journal on Software Tools for Technology Transfer, 23(6):867–870, 2021

    2019

  13. [13]

    Analyzing semantic correctness with symbolic execution: A case study on pkcs# 1 v1

    Sze Yiu Chau, Moosa Yahyazadeh, Omar Chowdhury, Aniket Kate, and Ninghui Li. Analyzing semantic correctness with symbolic execution: A case study on pkcs# 1 v1. 5 signature verification. In Network and Distributed Systems Security (NDSS) Symposium 2019, 2019

    2019

  14. [14]

    Simulation-directed invariant mining for software verification

    Xueqi Cheng and Michael S Hsiao. Simulation-directed invariant mining for software verification. InProceedings of the conference on Design, automation and test in Europe, pages 682–687, 2008

    2008

  15. [15]

    Counterexample-guided abstraction refinement

    Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. InInterna- tional Conference on Computer Aided Verification, pages 154–169. Springer, 2000

    2000

  16. [16]

    Dytan: a generic dynamic taint analysis framework

    James Clause, Wanchun Li, and Alessandro Orso. Dytan: a generic dynamic taint analysis framework. InProceedings of the 2007 international symposium on Software testing and analysis, pages 196– 206, 2007

    2007

  17. [17]

    Abstract interpretation.ACM Computing Surveys (CSUR), 28(2):324–328, 1996

    Patrick Cousot. Abstract interpretation.ACM Computing Surveys (CSUR), 28(2):324–328, 1996

    1996

  18. [18]

    Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

    Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. InProceedings of the 4th ACM SIGACT- SIGPLAN symposium on Principles of programming languages, pages 238–252, 1977

    1977

  19. [19]

    Abstract interpretation: past, present and future

    Patrick Cousot and Radhia Cousot. Abstract interpretation: past, present and future. InProceedings of the Joint Meeting of the Twenty- Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–10, 2014

    2014

  20. [20]

    Frama-c: A software analysis perspective

    Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-c: A software analysis perspective. InInternational conference on software engineering and formal methods, pages 233–247. Springer, 2012

    2012

  21. [21]

    Binsec/rel: Efficient relational symbolic execution for constant-time at binary- level

    Lesly-Ann Daniel, S ´ebastien Bardin, and Tamara Rezk. Binsec/rel: Efficient relational symbolic execution for constant-time at binary- level. In2020 IEEE Symposium on Security and Privacy (SP), pages 1021–1038. IEEE, 2020

    2020

  22. [22]

    Solving complex path conditions through heuristic search on induced polytopes

    Peter Dinges and Gul Agha. Solving complex path conditions through heuristic search on induced polytopes. InProceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 425–436, 2014

    2014

  23. [23]

    Exposing the rat in the tunnel: Using traffic analysis for tor-based malware detection

    Priyanka Dodia, Mashael AlSabah, Omar Alrawi, and Tao Wang. Exposing the rat in the tunnel: Using traffic analysis for tor-based malware detection. InProceedings of the 2022 ACM SIGSAC Con- ference on Computer and Communications Security, pages 875–889, 2022

    2022

  24. [24]

    F-droid: Free and open source android app reposi- tory

    F-Droid Project. F-droid: Free and open source android app reposi- tory. https://f-droid.org, 2026. Accessed: 2025-10-05

    2026

  25. [25]

    Android testing via synthetic symbolic execution

    Xiang Gao, Shin Hwei Tan, Zhen Dong, and Abhik Roychoudhury. Android testing via synthetic symbolic execution. InProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, pages 419–429, 2018

    2018

  26. [26]

    Adver- sities in abstract interpretation-accommodating robustness by abstract interpretation.ACM Transactions on Programming Languages and Systems, 46(2):1–31, 2024

    Roberto Giacobazzi, Isabella Mastroeni, and Elia Perantoni. Adver- sities in abstract interpretation-accommodating robustness by abstract interpretation.ACM Transactions on Programming Languages and Systems, 46(2):1–31, 2024

    2024

  27. [27]

    Dart: Directed au- tomated random testing

    Patrice Godefroid, Nils Klarlund, and Koushik Sen. Dart: Directed au- tomated random testing. InProceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, pages 213–223, 2005

    2005

  28. [28]

    Program analysis as constraint solving

    Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan. Program analysis as constraint solving. InProceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 281–292, 2008

    2008

  29. [29]

    When to stop? towards efficient code generation in llms with excess token prevention

    Lianghong Guo, Yanlin Wang, Ensheng Shi, Wanjun Zhong, Hongyu Zhang, Jiachi Chen, Ruikai Zhang, Yuchi Ma, and Zibin Zheng. When to stop? towards efficient code generation in llms with excess token prevention. InProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 1073–1085, 2024

    2024

  30. [30]

    Lazy counterfactual symbolic execution

    William T Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala, and Ruzica Piskac. Lazy counterfactual symbolic execution. In Proceedings of the 40th acm sigplan conference on programming language design and implementation, pages 411–424, 2019

    2019

  31. [31]

    Learning to fuzz from symbolic execution with application to smart contracts

    Jingxuan He, Mislav Balunovi ´c, Nodar Ambroladze, Petar Tsankov, and Martin Vechev. Learning to fuzz from symbolic execution with application to smart contracts. InProceedings of the 2019 ACM SIGSAC conference on computer and communications security, pages 531–548, 2019

    2019

  32. [32]

    Learning to explore paths for symbolic execution

    Jingxuan He, Gishor Sivanrupan, Petar Tsankov, and Martin Vechev. Learning to explore paths for symbolic execution. InProceedings of the 2021 ACM SIGSAC Conference on Computer and Communica- tions Security, pages 2526–2540, 2021

    2021

  33. [33]

    Model execution tracing: a sys- tematic mapping study.Software and Systems Modeling, 2019

    Fazilat Hojaji, Tanja Mayerhofer, Bahman Zamani, Abdelwahab Hamou-Lhadj, and Erwan Bousse. Model execution tracing: a sys- tematic mapping study.Software and Systems Modeling, 2019

    2019

  34. [34]

    Enhancing reuse of constraint solutions to improve symbolic execution

    Xiangyang Jia, Carlo Ghezzi, and Shi Ying. Enhancing reuse of constraint solutions to improve symbolic execution. InProceedings of the 2015 International Symposium on Software Testing and Analysis, pages 177–187, 2015

    2015

  35. [35]

    Neurlux: dynamic malware analysis without feature engineering

    Chani Jindal, Christopher Salls, Hojjat Aghakhani, Keith Long, Christopher Kruegel, and Giovanni Vigna. Neurlux: dynamic malware analysis without feature engineering. InProceedings of the 35th Annual Computer Security Applications Conference, pages 444–455, 2019

    2019

  36. [36]

    Codellm-devkit: A framework for contextualizing code llms with program analysis insights

    Rahul Krishna, Rangeet Pan, Saurabh Sinha, Srikanth Tamilselvam, Raju Pavuluri, and Maja Vukovic. Codellm-devkit: A framework for contextualizing code llms with program analysis insights. InProceed- ings of the 33rd ACM International Conference on the Foundations of Software Engineering, pages 308–318, 2025

    2025

  37. [37]

    Abstract execution: A technique for efficiently tracing programs.Software: Practice and Experience, 20(12):1241–1258, 1990

    James R Larus. Abstract execution: A technique for efficiently tracing programs.Software: Practice and Experience, 20(12):1241–1258, 1990

    1990

  38. [38]

    Mining temporal properties of data invariants

    Caroline Lemieux. Mining temporal properties of data invariants. In 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, volume 2, pages 751–753. IEEE, 2015

    2015

  39. [39]

    Revisiting concept drift in windows malware detection: Adaptation to real drifted malware with minimal samples.arXiv preprint arXiv:2407.13918, 2024

    Adrian Shuai Li, Arun Iyengar, Ashish Kundu, and Elisa Bertino. Revisiting concept drift in windows malware detection: Adaptation to real drifted malware with minimal samples.arXiv preprint arXiv:2407.13918, 2024

    work page arXiv 2024

  40. [40]

    Foredroid: Scenario-aware analysis for android malware detection and explanation

    Jiaming Li, Sen Chen, Chunlian Wu, Yuxin Zhang, and Lingling Fan. Foredroid: Scenario-aware analysis for android malware detection and explanation. InProceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security, pages 1379–1393, 2025

    2025

  41. [41]

    Symbolic execution of complex program driven by machine learning based constraint solving

    Xin Li, Yongjuan Liang, Hong Qian, Yi-Qi Hu, Lei Bu, Yang Yu, Xin Chen, and Xuandong Li. Symbolic execution of complex program driven by machine learning based constraint solving. InProceed- ings of the 31st IEEE/ACM International Conference on Automated Software Engineering, pages 554–559, 2016

    2016

  42. [42]

    Mining invariants from console logs for system problem detection

    Jian-Guang Lou, Qiang Fu, Shenqi Yang, Ye Xu, and Jiang Li. Mining invariants from console logs for system problem detection. In2010 USENIX Annual Technical Conference (USENIX ATC 10), 2010

    2010

  43. [43]

    System service call- oriented symbolic execution of android framework with applications to vulnerability discovery and exploit generation

    Lannan Luo, Qiang Zeng, Chen Cao, Kai Chen, Jian Liu, Limin Liu, Neng Gao, Min Yang, Xinyu Xing, and Peng Liu. System service call- oriented symbolic execution of android framework with applications to vulnerability discovery and exploit generation. InProceedings of the 15th Annual International Conference on Mobile Systems, Applications, and Services, pa...

    2017

  44. [44]

    Type-constrained code generation with language models.Proceedings of the ACM on Programming Languages, 9(PLDI):601–626, 2025

    Niels M ¨undler, Jingxuan He, Hao Wang, Koushik Sen, Dawn Song, and Martin Vechev. Type-constrained code generation with language models.Proceedings of the ACM on Programming Languages, 9(PLDI):601–626, 2025

    2025

  45. [45]

    Using an llm to help with code un- derstanding

    Daye Nam, Andrew Macvean, Vincent Hellendoorn, Bogdan Vasilescu, and Brad Myers. Using an llm to help with code un- derstanding. InProceedings of the IEEE/ACM 46th International Conference on Software Engineering, pages 1–13, 2024

    2024

  46. [46]

    Dynamic taint analysis for automatic detection, analysis, and signaturegeneration of exploits on commodity software

    James Newsome and Dawn Xiaodong Song. Dynamic taint analysis for automatic detection, analysis, and signaturegeneration of exploits on commodity software. InNDSS, volume 5, pages 3–4, 2005

    2005

  47. [47]

    Symbolic execution and recent applications to worst-case execution, load testing, and security analysis.Advances in Computers, 113:289–314, 2019

    Corina S P ˘as˘areanu, Rody Kersten, Kasper Luckow, and Quoc-Sang Phan. Symbolic execution and recent applications to worst-case execution, load testing, and security analysis.Advances in Computers, 113:289–314, 2019

    2019

  48. [48]

    Symbolic pathfinder: inte- grating symbolic execution with model checking for java bytecode analysis.Automated Software Engineering, 20(3):391–425, 2013

    Corina S P ˘as˘areanu, Willem Visser, David Bushnell, Jaco Gelden- huys, Peter Mehlitz, and Neha Rungta. Symbolic pathfinder: inte- grating symbolic execution with model checking for java bytecode analysis.Automated Software Engineering, 20(3):391–425, 2013

    2013

  49. [49]

    Enhancing symbolic execution of heap-based pro- grams with separation logic for test input generation

    Long H Pham, Quang Loc Le, Quoc-Sang Phan, Jun Sun, and Shengchao Qin. Enhancing symbolic execution of heap-based pro- grams with separation logic for test input generation. InInternational Symposium on Automated Technology for Verification and Analysis, pages 209–227. Springer, 2019

    2019

  50. [50]

    Symbolic execution with SymCC: Don’t interpret, compile! In29th USENIX Security Symposium (USENIX Security 20), pages 181–198

    Sebastian Poeplau and Aur ´elien Francillon. Symbolic execution with SymCC: Don’t interpret, compile! In29th USENIX Security Symposium (USENIX Security 20), pages 181–198. USENIX As- sociation, August 2020. URL: https://www.usenix.org/conference/ usenixsecurity20/presentation/poeplau

    2020

  51. [51]

    Symqemu: Compilation- based symbolic execution for binaries

    Sebastian Poeplau and Aur ´elien Francillon. Symqemu: Compilation- based symbolic execution for binaries. InNdss 2021, network and distributed system security symposium. Internet Society, 2021

    2021

  52. [52]

    Sentence-BERT: Sentence Embeddings using Siamese BERT-Networks

    Nils Reimers and Iryna Gurevych. Sentence-bert: Sentence embed- dings using siamese bert-networks.arXiv preprint arXiv:1908.10084, 2019

    work page internal anchor Pith review Pith/arXiv arXiv 1908

  53. [53]

    Unmasking the veiled: A comprehen- sive analysis of android evasive malware

    Antonio Ruggia, Dario Nisi, Savino Dambra, Alessio Merlo, Davide Balzarotti, and Simone Aonzo. Unmasking the veiled: A comprehen- sive analysis of android evasive malware. InProceedings of the 19th ACM Asia Conference on Computer and Communications Security, pages 383–398, 2024

    2024

  54. [54]

    Cute and jcute: Concolic unit testing and explicit path model-checking tools: (tool paper)

    Koushik Sen and Gul Agha. Cute and jcute: Concolic unit testing and explicit path model-checking tools: (tool paper). InInternational Conference on Computer Aided Verification, pages 419–423. Springer, 2006

    2006

  55. [55]

    SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis

    Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Audrey Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Kruegel, and Giovanni Vigna. SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis. InIEEE Symposium on Security and Privacy, 2016

    2016

  56. [56]

    Soot - a java bytecode optimization framework

    Raja Vall ´ee-Rai, Phong Co, Etienne Gagnon, Laurie Hendren, Patrick Lam, and Vijay Sundaresan. Soot - a java bytecode optimization framework. InProceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research, pages 13–23, 1999

    1999

  57. [57]

    Virusshare malware repository

    VirusShare. Virusshare malware repository. https://virusshare.com. Accessed: 2025

    2025

  58. [58]

    Exploring large language models for semantic analysis and categorization of android malware

    Brandon J Walton, Mst Eshita Khatun, James M Ghawaly, and Aisha Ali-Gombe. Exploring large language models for semantic analysis and categorization of android malware. In2024 Annual Computer Security Applications Conference Workshops (ACSAC Workshops), pages 248–254. IEEE, 2024

    2024

  59. [59]

    Testeval: Benchmarking large language models for test case generation

    Wenhan Wang, Chenyuan Yang, Zhijie Wang, Yuheng Huang, Zhaoyang Chu, Da Song, Lingming Zhang, An Ran Chen, and Lei Ma. Testeval: Benchmarking large language models for test case generation. InFindings of the Association for Computational Linguistics: NAACL 2025, pages 3547–3562, 2025

    2025

  60. [60]

    Symgx: Detecting cross-boundary pointer vulnerabilities of sgx applications via static symbolic execution

    Yuanpeng Wang, Ziqi Zhang, Ningyu He, Zhineng Zhong, Shengjian Guo, Qinkun Bao, Ding Li, Yao Guo, and Xiangqun Chen. Symgx: Detecting cross-boundary pointer vulnerabilities of sgx applications via static symbolic execution. InProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, pages 2710–2724, 2023

    2023

  61. [61]

    Symbolic execution of obfus- cated code

    Babak Yadegari and Saumya Debray. Symbolic execution of obfus- cated code. InProceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, pages 732–744, 2015

    2015

  62. [62]

    A comprehensive evaluation of android icc resolution techniques

    Jiwei Yan, Shixin Zhang, Yepang Liu, Xi Deng, Jun Yan, and Jian Zhang. A comprehensive evaluation of android icc resolution techniques. InProceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering, pages 1–13, 2022

    2022

  63. [63]

    Empc: Effective path prioritization for symbolic execution with path cover

    Shuangjie Yao and Dongdong She. Empc: Effective path prioritization for symbolic execution with path cover. In2025 IEEE Symposium on Security and Privacy (SP), pages 2995–3013. IEEE, 2025

    2025

  64. [64]

    A comprehensive survey on automatic text summarization with explo- ration of llm-based methods.Neurocomputing, page 131928, 2025

    Yang Zhang, Hanlei Jin, Dan Meng, Jun Wang, and Jinghua Tan. A comprehensive survey on automatic text summarization with explo- ration of llm-based methods.Neurocomputing, page 131928, 2025

    2025

  65. [65]

    Ferry: State-Aware symbolic execution for exploring State-Dependent program paths

    Shunfan Zhou, Zhemin Yang, Dan Qiao, Peng Liu, Min Yang, Zhe Wang, and Chenggang Wu. Ferry: State-Aware symbolic execution for exploring State-Dependent program paths. In31st USENIX Se- curity Symposium (USENIX Security 22), pages 4365–4382, Boston, MA, August 2022. USENIX Association. URL: https://www.usenix. org/conference/usenixsecurity22/presentation/...

    2022

  66. [66]

    Analyze conditional statements in Android Jimple bytecode to determine execution constraints for target method reachability

    Task:You are an expert static analysis engineer specializing in Android bytecode constraint extraction. Analyze conditional statements in Android Jimple bytecode to determine execution constraints for target method reachability

  67. [67]

    Input:{{conditional_node}}— Conditional node from CFG {{target_node}}— Target node or Target method callsite {{method_bytecode}}— Complete Jimple bytecode of containing method

  68. [68]

    Instructions:(1) Trace variables to recent assignments, (2) Interpret framework method semantics, (3) Determine branch direction (TRUE/FALSE/CASE X), (4) Replace byte- code names with semantic equivalents, (5) Generate boolean logic and human-readable constraints

  69. [69]

    branch_direction

    Output:Provide response in this exact JSON format: { "branch_direction": "TRUE|FALSE|CASE_X", "variable_mappings":{"original_name": "semantic_name"}, "framework_methods": [{"method": "name", "purpose": "function"}], "boolean_constraint": "semantic_variable == value", "business_constraint": "Human readable requirement" } Figure 4. LLM prompt template for s...