Symbolon: Symbolic Execution by Learning Code Transformation

• URL: http://arxiv.org/abs/2606.29108v1
• Date: Sat, 27 Jun 2026 23:16:50 GMT
• Title: Symbolon: Symbolic Execution by Learning Code Transformation
• Abstract summary: We present Symbolon, a framework that learns diverse code transformations and applies them context-sensitively to improve symbolic execution.<n>Our evaluation shows that Symbolon substantially improves the symbolic execution engine KLEE across 16 search strategies on 32 real-world programs.
• Score: 20.89743100548855
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Symbolic execution is a powerful program analysis technique with broad applications, such as vulnerability detection, security testing, and malware analysis. However, this technique is known to suffer from scalability issues, e.g., path explosion, complex constraints, due to certain structural and semantic patterns commonly presented in real-world programs. Existing approaches attempt to escape these patterns by transforming programs into new representations to reduce the execution cost. Unfortunately, these transformations are often too rigid to exploit diverse local program semantics and sometimes rely on compiler optimizations designed for concrete execution that may misalign with the goals of symbolic execution. We present Symbolon, a framework that automatically learns diverse code transformations and applies them context-sensitively to improve symbolic execution. Our key insight is to formulate transformation discovery as a search problem over program representations. To make the search practical, Symbolon learns transformations cheaply offline on small programs, distills them into a reusable library of agent skills, and uses an agent to instantiate these skills on repo-level targets. Our evaluation shows that Symbolon substantially improves the symbolic execution engine KLEE across 16 search strategies on 32 real-world programs, increasing line coverage by 3.69x on average while reducing peak memory and per-query solver time by 29.2x and 123x, respectively. When applied to the latest Linux kernel, Symbolon uncovers 21 previously unknown bugs, all of which have been reported to the kernel maintainers.

Related papers

• Overcoming the Weakest-Link Effect in LLM-Driven Program Optimization via Heterogeneous Edit Recombination [59.679182823718556]
  HERO is a program that generates diverse, non-overlapping atomic edits and then systematically selects and composes them into coherent program improvements using evaluator scores.<n>We evaluate HERO across algorithmic problems, strategy games, the design of LLM-based agentic systems, and robotic path planning.
  arXiv  Detail & Related papers  (2026-07-31T02:05:45Z)
• Can LLMs Recover Program Semantics? A Systematic Evaluation with Symbolic Execution [1.5377279217726239]
  Obfuscation poses a persistent challenge for software engineering tasks such as program comprehension, maintenance, testing, and vulnerability detection.<n>We investigate whether fine-tuned language models can effectively deobfuscate programs and restore analyzability.
  arXiv  Detail & Related papers  (2025-11-24T13:55:20Z)
• Symbolic Execution in Practice: A Survey of Applications in Vulnerability, Malware, Firmware, and Protocol Analysis [3.1844358655583846]
  Symbolic execution is a powerful program analysis technique that allows for the systematic exploration of all program paths.<n>This paper introduces a systematic taxonomy of strategies to enable symbolic execution on complex software systems.<n>We survey applications of symbolic executions in several domains such as vulnerability analysis, malware analysis, firmware re-hosting, and network protocol analysis.
  arXiv  Detail & Related papers  (2025-08-08T18:43:45Z)
• LIFT: Automating Symbolic Execution Optimization with Large Language Models for AI Networks [31.69036961288122]
  LIFT (Large-language-model Integrated Functional-equivalent-IR Transformation) is a novel framework that automates the optimization of Intermediate Representations (IRs) in symbolic execution.<n> Experiments on real-world binaries demonstrated significant performance improvements.
  arXiv  Detail & Related papers  (2025-07-07T12:26:56Z)
• Exposing Go's Hidden Bugs: A Novel Concolic Framework [2.676686591720132]
  We present Zorya, a novel methodology to evaluate Go programs comprehensively.<n>By systematically exploring execution paths to uncover vulnerabilities beyond conventional testing, symbolic execution offers distinct advantages.<n>Our solution employs Ghidra's P-Code as an intermediate representation (IR)
  arXiv  Detail & Related papers  (2025-05-26T16:26:20Z)
• ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
  The goal of decompilation is to convert compiled low-level code (e.g., assembly code) back into high-level programming languages.<n>This task supports various reverse engineering applications, such as vulnerability identification, malware analysis, and legacy software migration.
  arXiv  Detail & Related papers  (2025-02-17T12:38:57Z)
• ReGAL: Refactoring Programs to Discover Generalizable Abstractions [59.05769810380928]
  Generalizable Abstraction Learning (ReGAL) is a method for learning a library of reusable functions via codeization. We find that the shared function libraries discovered by ReGAL make programs easier to predict across diverse domains. For CodeLlama-13B, ReGAL results in absolute accuracy increases of 11.5% on LOGO, 26.1% on date understanding, and 8.1% on TextCraft, outperforming GPT-3.5 in two of three domains.
  arXiv  Detail & Related papers  (2024-01-29T18:45:30Z)
• Divide, Conquer and Verify: Improving Symbolic Execution Performance [0.0]
  Symbolic Execution is a formal method that can be used to verify the behavior of computer programs and detect software vulnerabilities.<n>Despite advances in performance in recent years, Symbolic Execution is too slow to be applied to real-world software.<n>We present a divide-and-conquer approach for symbolic execution by executing individual slices and later combining the side effects.
  arXiv  Detail & Related papers  (2023-10-05T15:21:10Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  Learned transpilation offers an alternative to manual re-writing and engineering efforts. Probabilistic neural language models (LMs) produce plausible outputs for every input, but do so at the cost of guaranteed correctness. Guess & Sketch extracts alignment and confidence information from features of the LM then passes it to a symbolic solver to resolve semantic equivalence.
  arXiv  Detail & Related papers  (2023-09-25T15:42:18Z)
• Symbolic Visual Reinforcement Learning: A Scalable Framework with Object-Level Abstraction and Differentiable Expression Search [63.3745291252038]
  We propose DiffSES, a novel symbolic learning approach that discovers discrete symbolic policies. By using object-level abstractions instead of raw pixel-level inputs, DiffSES is able to leverage the simplicity and scalability advantages of symbolic expressions. Our experiments demonstrate that DiffSES is able to generate symbolic policies that are simpler and more scalable than state-of-the-art symbolic RL methods.
  arXiv  Detail & Related papers  (2022-12-30T17:50:54Z)
• High-performance symbolic-numerics via multiple dispatch [52.77024349608834]
  Symbolics.jl is an extendable symbolic system which uses dynamic multiple dispatch to change behavior depending on the domain needs. We show that by formalizing a generic API on actions independent of implementation, we can retroactively add optimized data structures to our system. We demonstrate the ability to swap between classical term-rewriting simplifiers and e-graph-based term-rewriting simplifiers.
  arXiv  Detail & Related papers  (2021-05-09T14:22:43Z)

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.