RECON: An LLM-Enhanced Backward Constraint Analysis Framework

• URL: http://arxiv.org/abs/2606.10264v1
• Date: Tue, 09 Jun 2026 00:09:50 GMT
• Title: RECON: An LLM-Enhanced Backward Constraint Analysis Framework
• Abstract summary: In this paper, we present a novel large language model (LLM)-enhanced backward constraint analysis framework.<n>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.<n>Results demonstrate that our approach operates 5.8X faster than traditional symbolic execution, with a 100% success rate, while maintaining logical equivalence.
• Score: 0.5424799109837065
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• The Imitation Game: When LLMs Learn to Reason Like Programs via Code-Centric Reasoning Data Synthesis [50.473217152006875]
  MIMIC is a framework that leverages executable code as a rigorous medium for reasoning data synthesis.<n>MIMIC transforms algorithms into verifiable reasoning trajectories through narrative fusion, code-guided test synthesis, and dynamic code instrumentation.<n>Our method significantly elevates accuracy across general reasoning, complex mathematical benchmarks, and fine-grained deterministic tasks.
  arXiv  Detail & Related papers  (2026-09-13T17:04:16Z)
• RepoReasoner: Evaluating Repository-Level Code Reasoning Ability of Long-Context Language Models [54.53236295237077]
  We introduce RepoReasoner, a benchmark for evaluating repository-level code reasoning.<n> Output Prediction measures fine-grained, stateful execution reasoning across files.<n>Call Chain Prediction evaluates high-level architectural dependency understanding under noisy context.
  arXiv  Detail & Related papers  (2026-07-28T17:12:41Z)
• Feedback-Driven Execution for LLM-Based Binary Analysis [6.612857121548629]
  We present FORGE, a system that rethinks LLM-based analysis as a feedback-driven execution process.<n> FORGE interleaves reasoning and tool interaction through a reasoning-action-observation loop.<n>We evaluate FORGE on 3,457 real-world firmware binaries.
  arXiv  Detail & Related papers  (2026-04-16T15:15:58Z)
• Evaluating the Formal Reasoning Capabilities of Large Language Models through Chomsky Hierarchy [62.32144504442516]
  It is unknown whether SOTA LLMs can grasp the structured, hierarchical complexity of formal languages.<n>ChomskyBench is a benchmark for systematically evaluating LLMs through the lens of Chomsky Hierarchy.<n>ChomskyBench is composed of a comprehensive suite of language recognition and generation tasks designed to test capabilities at each level.
  arXiv  Detail & Related papers  (2026-04-03T04:06:39Z)
• Understanding by Reconstruction: Reversing the Software Development Process for LLM Pretraining [66.89012795621349]
  Large Language Models (LLMs) often struggle with the deep, long-horizon reasoning required for complex software engineering.<n>We propose a novel paradigm: understanding via reconstruction.<n>We introduce a framework that synthesizes latent agentic trajectories using a multi-agent simulation.
  arXiv  Detail & Related papers  (2026-03-11T09:23:20Z)
• Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code [2.0890922389987683]
  Gordian is a hybrid symbolic execution framework.<n>It generates lightweight ghost code that aids an SMT solver in handling solver-hostile code fragments.<n>It improves coverage on average by 52-84% over traditional symbolic execution baselines.
  arXiv  Detail & Related papers  (2026-01-31T07:14:57Z)
• VIRO: Robust and Efficient Neuro-Symbolic Reasoning with Verification for Referring Expression Comprehension [51.76841625486355]
  Referring Expression (REC) aims to localize the image region corresponding to a natural-language query.<n>Recent neuro-symbolic REC approaches leverage large language models (LLMs) and vision-language models (VLMs) to perform compositional reasoning.<n>We introduce VIRO, a neuro-symbolic framework that embeds lightweight operator-level verifiers within reasoning steps.
  arXiv  Detail & Related papers  (2026-01-19T07:21:19Z)
• From Brute Force to Semantic Insight: Performance-Guided Data Transformation Design with LLMs [48.83701310501069]
  Large language models (LLMs) have achieved notable performance in code synthesis.<n>We introduce a performance-aware, closed-loop solution that enables LLMs to autonomously engineer optimal transformations.<n>We fine-tune LLMs with Low-Rank Adaptation on a novel repository of more than 6,000 empirically evaluated PyTorch augmentation functions.
  arXiv  Detail & Related papers  (2026-01-07T11:13:02Z)
• KBQA-R1: Reinforcing Large Language Models for Knowledge Base Question Answering [64.62317305868264]
  We present textbfKBQA-R1, a framework that shifts the paradigm from text imitation to interaction optimization via Reinforcement Learning.<n>Treating KBQA as a multi-turn decision process, our model learns to navigate the knowledge base using a list of actions.<n>Experiments on WebQSP, GrailQA, and GraphQuestions demonstrate that KBQA-R1 achieves state-of-the-art performance.
  arXiv  Detail & Related papers  (2025-12-10T17:45:42Z)
• Can Large Language Models Solve Path Constraints in Symbolic Execution? [32.45630887872447]
  We focus on investigating the possibility of adopting large language models (LLM) for path constraint solving.<n>We build new evaluation pipelines and benchmarks for two tasks: test case generation and path classification.<n>Our experiment results show that state-of-the-art LLMs are able to solve path constraints in both generation and classification tasks.
  arXiv  Detail & Related papers  (2025-11-23T04:54:48Z)
• Worst-Case Symbolic Constraints Analysis and Generalisation with Large Language Models [7.658134651527103]
  Worst-case symbolic constraints analysis requires inferring the symbolic constraints that characterise worst-case program executions.<n>We show that even state-of-the-art large language models (LLMs) struggle when applied directly on this task.<n>We propose WARP, an innovative neurosymbolic approach that computes worst-case constraints on smaller concrete input sizes.
  arXiv  Detail & Related papers  (2025-06-09T19:33:30Z)
• SymRTLO: Enhancing RTL Code Optimization with LLMs and Neuron-Inspired Symbolic Reasoning [30.938876549335067]
  This paper presents SymRTLO, a novel neuron-symbolic RTL optimization framework.<n>A symbolic module is proposed for analyzing and optimizing finite state machine (FSM) logic.<n> Experiments on the RTL-Rewriter benchmark with Synopsys Design Compiler and Yosys show that SymRTLO improves power, performance, and area (PPA) by up to 43.9%, 62.5%, and 51.1%, respectively.
  arXiv  Detail & Related papers  (2025-04-14T16:15:55Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.