pith. sign in

arxiv: 2606.29108 · v1 · pith:7NHU6DNCnew · submitted 2026-06-27 · 💻 cs.CR · cs.PL· cs.SE

Symbolon: Symbolic Execution by Learning Code Transformation

Jie Zhu , Penghui Li , Zhongxuan Li , Chihao Shen , Ziyang Li , Yizheng Chen , Kexin Pei This is my paper

Pith reviewed 2026-06-30 09:04 UTC · model grok-4.3

classification 💻 cs.CR cs.PLcs.SE
keywords symbolic executioncode transformationprogram analysisvulnerability detectionKLEELinux kernelsearch-based learning
0
0 comments X

The pith

Symbolon learns code transformations on small programs and applies them via an agent to raise symbolic execution coverage on large targets.

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

The paper presents Symbolon as a way to overcome path explosion and complex constraints in symbolic execution by automatically discovering code transformations. It frames discovery as a search over program representations, performs that search cheaply on small programs, and distills the results into a library of reusable skills. An agent then instantiates those skills context-sensitively on full-scale targets, aiming to adapt to local semantics better than rigid or compiler-derived rewrites. A reader would care because the method targets the core scalability barrier that has limited symbolic execution's use on real software.

Core claim

Symbolon formulates transformation discovery as search on small programs, distills the outcomes into a library of agent skills, and uses an agent to apply the skills context-sensitively on repo-level targets, thereby improving symbolic execution engines such as KLEE.

What carries the argument

a reusable library of agent skills distilled from offline search-based transformation discovery on small programs and instantiated context-sensitively by an agent

If this is right

  • KLEE with Symbolon raises average line coverage 3.69 times across 32 real-world programs and 16 search strategies.
  • Peak memory usage falls by a factor of 29.2 and per-query solver time by a factor of 123.
  • The framework identifies 21 previously unknown bugs in the latest Linux kernel, all reported to maintainers.

Where Pith is reading between the lines

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

  • The same distilled-skill approach could be tried on other symbolic execution engines to check whether the coverage and resource gains transfer.
  • If the skills generalize, they might be tested as a preprocessing step for related techniques such as concolic execution.
  • Collecting a broader set of small programs for the initial search phase could increase the range of programs that benefit from the skill library.

Load-bearing premise

Transformations found through search on small programs can be turned into skills that an agent applies to much larger programs while preserving their effectiveness and semantic correctness.

What would settle it

An experiment on the same 32 programs showing that Symbolon produces no measurable gain in line coverage, peak memory, or solver time over unmodified KLEE across the 16 search strategies.

Figures

Figures reproduced from arXiv: 2606.29108 by Chihao Shen, Jie Zhu, Kexin Pei, Penghui Li, Yizheng Chen, Zhongxuan Li, Ziyang Li.

Figure 1
Figure 1. Figure 1: A motivating example from libtiff showing how Symbolon helps symbolic execution by transforming the code. Each node in an execution trace represents an execution state, and each edge denotes a transition between two states. Nodes with dashed borders indicate states that are no longer explored in Symbolon. ing states when the size cannot be bounded or modeled. Therefore, exploration may stop before reaching… view at source ↗
Figure 2
Figure 2. Figure 2: Overview of the Symbolon workflow. In the offline learning phase, Symbolon runs symbolic execution on simple programs and uses evolutionary search to learn a diverse collection of transformations. These transformations are then distilled into agent skills, which are further packaged into a reusable skill library for online inference to real-world programs. suring progress on the original program. This crea… view at source ↗
Figure 3
Figure 3. Figure 3: Per-program line coverage across 16 search strategies after 12 hours. Each subplot shows one program. Bars follow the legend order. For each bar, the dark segment represents baseline coverage, and the light segment represents additional coverage obtained from Symbolon under the same strategy. The ratio in each subplot title is Symbolon’s average improvement on that program across all strategies, while the … view at source ↗
Figure 4
Figure 4. Figure 4: Line coverage of Symbolon under different compiler-optimization flags. Each bar is one flag (color); the solid base is the baseline coverage with that flag and the lighter cap is the additional lines Symbolon covers. Titles report the per-program improvement ratio. tably, Symbolon also reduces the dependence on the choice of search strategy. On the original programs, the strongest strategy covers 7.4× as m… view at source ↗
Figure 5
Figure 5. Figure 5: Two representative bugs exposed by Symbolon-generated tests and missed by the evaluated baselines under the same budget. (a) An ASan-reported stack overflow in flvmeta. (b) An out-of-bounds access in Linux JFS that can corrupt kernel memory or trigger a crash [PITH_FULL_IMAGE:figures/full_fig_p012_5.png] view at source ↗
read the original 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.

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

1 major / 2 minor

Summary. The paper presents Symbolon, a framework for improving symbolic execution by automatically learning code transformations. It formulates transformation discovery as a search problem over program representations, performs cheap offline search on small programs, distills the results into a reusable library of agent skills, and deploys an agent to apply the skills context-sensitively on large repo-scale targets. The central empirical claim is that Symbolon improves the KLEE engine across 16 search strategies on 32 real-world programs (3.69× average line coverage, 29.2× peak memory reduction, 123× per-query solver time reduction) and, when applied to the latest Linux kernel, discovers 21 previously unknown bugs that were reported to maintainers.

Significance. If the results hold, the work would constitute a meaningful advance in symbolic execution by replacing rigid, hand-crafted or compiler-oriented transformations with an automated, learnable pipeline that adapts to local program semantics. The evaluation on a diverse set of 32 programs, multiple search strategies, and a production-scale target (Linux kernel) with concrete bug reports supplies falsifiable, practical evidence. The offline-learning-plus-online-instantiation design is a clear strength that could be reused in other program-analysis settings.

major comments (1)
  1. [Abstract and pipeline description (Section 3)] The performance and bug-finding claims rest on the assumption that the learned transformations preserve semantics. The abstract and the description of the distillation/instantiation pipeline supply no mechanism (e.g., equivalence checking, differential testing, or constraint-structure preservation) that would guarantee the transformed program is observationally equivalent to the original. Because every reported metric (coverage, memory, solver time, and new bugs) is only interpretable under semantic preservation, this omission is load-bearing for the central claim.
minor comments (2)
  1. [Abstract] The abstract states gains “across 16 search strategies” but does not enumerate the strategies or the selection criteria; adding this list (or a pointer to the experimental-setup subsection) would improve reproducibility.
  2. [Evaluation section] Table or figure captions that report the 3.69× / 29.2× / 123× figures should explicitly state the baseline (vanilla KLEE) and whether the numbers are arithmetic means, geometric means, or medians.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive feedback and the opportunity to address this important point regarding semantic preservation. We respond to the major comment below.

read point-by-point responses

  1. Referee: [Abstract and pipeline description (Section 3)] The performance and bug-finding claims rest on the assumption that the learned transformations preserve semantics. The abstract and the description of the distillation/instantiation pipeline supply no mechanism (e.g., equivalence checking, differential testing, or constraint-structure preservation) that would guarantee the transformed program is observationally equivalent to the original. Because every reported metric (coverage, memory, solver time, and new bugs) is only interpretable under semantic preservation, this omission is load-bearing for the central claim.

    Authors: We agree that semantic preservation is foundational to interpreting all reported metrics and that the current abstract and Section 3 description do not make the verification mechanism explicit. The search process operates exclusively on small programs for which we perform differential testing (comparing concrete and symbolic outputs before and after each candidate transformation) to retain only semantics-preserving rewrites; these verified transformations are then distilled into the skill library. However, we acknowledge that this verification step is not described in the pipeline overview. In the revised manuscript we will add a dedicated subsection to Section 3 that details the differential-testing procedure used during offline search, including the concrete test harness, the equivalence criterion, and how it carries over to the online instantiation phase. This addition will make the preservation guarantee explicit without altering any experimental results. revision: yes

Circularity Check

0 steps flagged

No circularity: empirical claims rest on external measurements, not self-referential definitions or fitted predictions.

full rationale

The paper's core results are direct empirical measurements (line coverage, memory usage, solver time on 32 programs; 21 new bugs in the Linux kernel) obtained by running the transformed programs through KLEE. No equations, parameters, or uniqueness theorems are defined in terms of the target metrics; the learning step is presented as offline search whose outputs are then applied and measured externally. The generalization assumption (no semantic loss) is a methodological claim whose validity is tested by the reported outcomes rather than presupposed by construction. No self-citation chains or ansatzes reduce the reported gains to tautologies.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The framework rests on the domain assumption that useful transformations exist and can be discovered offline; it introduces the new entity of a distilled agent-skills library whose effectiveness is asserted by the reported empirical gains.

axioms (1)
  • domain assumption Program transformations discovered on small programs preserve the semantics needed for symbolic execution while reducing path and constraint cost.
    This assumption underpins the offline learning phase and the claim that the learned skills remain valid on large targets.
invented entities (1)
  • distilled agent skills library no independent evidence
    purpose: Reusable set of learned transformations that an agent can instantiate context-sensitively on large programs
    Introduced to make the search practical and to bridge offline learning with repo-level application.

pith-pipeline@v0.9.1-grok · 5803 in / 1376 out tokens · 43432 ms · 2026-06-30T09:04:52.997101+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

140 extracted references · 12 canonical work pages · 7 internal anchors

  1. [1]

    Symbolic execution and program testing,

    J. C. King, “Symbolic execution and program testing,”Commun. ACM, vol. 19, no. 7, p. 385–394, 1976

    1976

  2. [2]

    Symbolic execution for software testing in practice: preliminary assessment,

    C. Cadar, P. Godefroid, S. Khurshid, C. S. Păsăreanu, K. Sen, N. Till- mann, and W. Visser, “Symbolic execution for software testing in practice: preliminary assessment,” inProceedings of the 33rd Inter- national Conference on Software Engineering, 2011, pp. 1066–1071

    2011

  3. [3]

    KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs,

    C. Cadar, D. Dunbar, and D. R. Engler, “KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs,” inProceedings of the 8th USENIX Symposium on Op- erating Systems Design and Implementation (OSDI’08). USENIX Association, 2008, pp. 209–224

    2008

  4. [4]

    S2e: A platform for in-vivo multi-path analysis of software systems,

    V. Chipounov, V. Kuznetsov, and G. Candea, “S2e: A platform for in-vivo multi-path analysis of software systems,” inProceedings of the sixteenth international conference on Architectural support for programming languages and operating systems. ACM, 2011

    2011

  5. [5]

    Symbolic execution with SYMCC: don’t interpret, compile!

    S. Poeplau and A. Francillon, “Symbolic execution with SYMCC: don’t interpret, compile!” inProceedings of the 29th USENIX Con- ference on Security Symposium. USENIX Association, 2020, pp. 181–198

    2020

  6. [6]

    Rethinking pointer rea- soning in symbolic execution,

    E. Coppa, D. C. D’Elia, and C. Demetrescu, “Rethinking pointer rea- soning in symbolic execution,” inProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 2017, pp. 613–618

    2017

  7. [7]

    Advancing automated, permission-based pro- gram verification using symbolic execution,

    M. H. Schwerhoff, “Advancing automated, permission-based pro- gram verification using symbolic execution,” Ph.D. dissertation, ETH Zurich, 2016

    2016

  8. [8]

    Automated reasoning and detection of specious configuration in large systems with symbolic execution,

    Y. Hu, G. Huang, and P. Huang, “Automated reasoning and detection of specious configuration in large systems with symbolic execution,” inProceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20), 2020, pp. 719–734

    2020

  9. [9]

    Towards symbolic pointers reasoning in dynamic symbolic execution,

    D. Kuts, “Towards symbolic pointers reasoning in dynamic symbolic execution,” in2021 Ivannikov Memorial Workshop (IVMEM). IEEE, 2021, pp. 42–49

    2021

  10. [10]

    Droidreach++: Exploring the reachability of native code in android applications,

    L. Borzacchiello, M. Cornacchia, D. Maiorca, G. Giacinto, and E. Coppa, “Droidreach++: Exploring the reachability of native code in android applications,”Computers & Security, p. 104657, 2025

    2025

  11. [11]

    Dart: Directed automated random testing,

    P. Godefroid, N. Klarlund, and K. Sen, “Dart: Directed automated random testing,” inProceedings of the 2005 ACM SIGPLAN confer- ence on Programming language design and implementation, 2005, pp. 213–223

    2005

  12. [12]

    Directedincremental symbolic execution,

    S. Person,G. Yang,N. Rungta,andS. Khurshid,“Directedincremental symbolic execution,” inProceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011, pp. 504–515

    2011

  13. [13]

    Analyzing semantic correctness with symbolic execution: A case study on pkcs# 1 v1. 5 signature verification,

    S. Y. Chau, M. Yahyazadeh, O. Chowdhury, A. Kate, and N. Li, “Analyzing semantic correctness with symbolic execution: A case study on pkcs# 1 v1. 5 signature verification,” inNetwork and Distributed Systems Security (NDSS) Symposium 2019, 2019

    2019

  14. [14]

    Efficient state merging in symbolic execution,

    V. Kuznetsov, J. Kinder, S. Bucur, and G. Candea, “Efficient state merging in symbolic execution,” inProceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Im- plementation, 2012, pp. 193–204

    2012

  15. [15]

    Symbolic execution for randomized programs,

    Z. Susag, S. Lahiri, J. Hsu, and S. Roy, “Symbolic execution for randomized programs,”Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA2, pp. 1583–1612, 2022

    2022

  16. [16]

    Assisting malware analysis with symbolic execution: A case study,

    R. Baldoni, E. Coppa, D. C. D’Elia, and C. Demetrescu, “Assisting malware analysis with symbolic execution: A case study,” inInter- national conference on cyber security cryptography and machine learning. Springer, 2017, pp. 171–188

    2017

  17. [17]

    Driller: Augmenting fuzzing through selective symbolic execution

    N. Stephens, J. Grosen, C. Salls, A. Dutcher, R. Wang, J. Corbetta, Y. Shoshitaishvili, C. Kruegel, and G. Vigna, “Driller: Augmenting fuzzing through selective symbolic execution.” inNDSS, vol. 16, no. 2016, 2016, pp. 1–16

    2016

  18. [18]

    Savior: Towardsbug-driven hybridtesting,

    Y. Chen, P. Li, J. Xu, S. Guo, R. Zhou, Y. Zhang, T. Wei, and L. Lu, “Savior: Towardsbug-driven hybridtesting,”in2020IEEESymposium on Security and Privacy (SP). IEEE, 2020, pp. 1580–1596

    2020

  19. [19]

    Pangolin: Incre- mental hybrid fuzzing with polyhedral path abstraction,

    H. Huang, P. Yao, R. Wu, Q. Shi, and C. Zhang, “Pangolin: Incre- mental hybrid fuzzing with polyhedral path abstraction,” in2020 IEEE Symposium on Security and Privacy (SP). IEEE, 2020, pp. 1613–1627

    2020

  20. [20]

    SyzSpec: specification generation for linux kernel fuzzing via under-constrained symbolic execution,

    Y. Hao, J. Pu, X. Li, Z. Qian, and A. A. Sani, “SyzSpec: specification generation for linux kernel fuzzing via under-constrained symbolic execution,” inProceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, 2025, pp. 813–826

    2025

  21. [21]

    Sound and effi- cient generation of data-oriented exploits via programming language synthesis,

    Y. Ling, G. Rajiv, K. Gopinathan, and I. Sergey, “Sound and effi- cient generation of data-oriented exploits via programming language synthesis,” in34th USENIX Security Symposium (USENIX Security 25), 2025, pp. 413–429

    2025

  22. [22]

    Syml: Guiding symbolic execution toward vulnerable states through pattern learning,

    N. Ruaro, K. Zeng, L. Dresel, M. Polino, T. Bao, A. Continella, S. Zanero, C. Kruegel, and G. Vigna, “Syml: Guiding symbolic execution toward vulnerable states through pattern learning,” inPro- ceedings of the 24th International Symposium on Research in Attacks, Intrusions and Defenses, 2021, pp. 456–468. 14

    2021

  23. [23]

    Guiding Symbolic Execution with Static Analysis and LLMs for Vulnerability Discovery

    M. Shafiuzzaman, A. Desai, W. Guo, and T. Bultan, “Guiding sym- bolic execution with static analysis and llms for vulnerability discov- ery,”arXiv preprint arXiv:2604.06506, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  24. [24]

    Under-constrained symbolic execu- tion: Correctness checking for real code,

    D. A. Ramos and D. Engler, “Under-constrained symbolic execu- tion: Correctness checking for real code,” in24th USENIX Security Symposium (USENIX Security 15), 2015, pp. 49–64

    2015

  25. [25]

    Sys: A static/symbolic tool for finding good bugs in good (browser) code,

    F. Brown, D. Stefan, and D. Engler, “Sys: A static/symbolic tool for finding good bugs in good (browser) code,” in29th USENIX Security Symposium (USENIX Security 20), 2020, pp. 199–216

    2020

  26. [26]

    Maze: Towards automated heap feng shui,

    Y. Wang, C. Zhang, Z. Zhao, B. Zhang, X. Gong, and W. Zou, “Maze: Towards automated heap feng shui,” in30th USENIX security symposium (USENIX security 21), 2021, pp. 1647–1664

    2021

  27. [27]

    The taming of the stack: Isolating stack data from memory errors,

    K. Huang, Y. Huang, M. Payer, Z. Qian, J. Sampson, G. Tan, and T. Jaeger, “The taming of the stack: Isolating stack data from memory errors,” inNDSS, 2022

    2022

  28. [28]

    Symbisect: Accurate bisection for fuzzer-exposed vulnerabilities,

    Z. Zhang, Y. Hao, W. Chen, X. Zou, X. Li, H. Li, Y. Zhai, and B. Lau, “Symbisect: Accurate bisection for fuzzer-exposed vulnerabilities,” in 33rd USENIX Security Symposium (USENIX Security 24), 2024, pp. 2493–2510

    2024

  29. [29]

    The cost of performance: Breaking threadx with kernel object masquerading attacks,

    X. Shao, Z. Ling, Y. Zhang, H. Yan, Y. Wei, L. Luo, Z. Liu, J. Luo, and X. Fu, “The cost of performance: Breaking threadx with kernel object masquerading attacks,” in34th USENIX Security Symposium (USENIX Security 25), 2025, pp. 7507–7524

    2025

  30. [30]

    Rakis: Secure fast i/o primitives across trust boundaries on intel sgx,

    M. Alharthi, F. Sang, D. Kuvaiskii, M. Vij, and T. Kim, “Rakis: Secure fast i/o primitives across trust boundaries on intel sgx,” in Proceedings of the Twentieth European Conference on Computer Systems, 2025, pp. 1177–1193

    2025

  31. [31]

    Scad: Towards a universal and automated network side-channel vul- nerability detection,

    K. Man, Z. Wang, Y. Hao, S. Zheng, X. Zhou, Y. Cao, and Z. Qian, “Scad: Towards a universal and automated network side-channel vul- nerability detection,” in2025 IEEE Symposium on Security and Privacy (SP). IEEE, 2025, pp. 1861–1876

    2025

  32. [32]

    Hunting defi vulnerabilities via context-sensitive concolic verification,

    Y. Ding, A. Gervais, R. Wattenhofer, and H. Sato, “Hunting defi vulnerabilities via context-sensitive concolic verification,” inPro- ceedings of the 2024 IEEE/ACM 46th International Conference on Software Engineering: Companion Proceedings, 2024, pp. 324–325

    2024

  33. [33]

    Sage: whitebox fuzzing for security testing,

    P. Godefroid, M. Y. Levin, and D. Molnar, “Sage: whitebox fuzzing for security testing,”Commun. ACM, vol. 55, no. 3, p. 40–44, 2012

    2012

  34. [34]

    Billions and billions of constraints: whitebox fuzz testing in production,

    E. Bounimova, P. Godefroid, and D. Molnar, “Billions and billions of constraints: whitebox fuzz testing in production,” inProceedings of the 2013 International Conference on Software Engineering. IEEE Press, 2013, p. 122–131

    2013

  35. [35]

    Pex: white box test generation for .net,

    N. Tillmann and J. De Halleux, “Pex: white box test generation for .net,” inProceedings of the 2nd International Conference on Tests and Proofs. Springer-Verlag, 2008, p. 134–153

    2008

  36. [36]

    Transferring an automated test generation tool to practice: from pex to fakes and code digger,

    N. Tillmann, J. de Halleux, and T. Xie, “Transferring an automated test generation tool to practice: from pex to fakes and code digger,” inProceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering. Association for Computing Machinery, 2014, p. 385–396

    2014

  37. [37]

    Higher-order test generation,

    P. Godefroid, “Higher-order test generation,”SIGPLAN Not., vol. 46, no. 6, p. 258–269, 2011

    2011

  38. [38]

    Boot- stomp: On the security of bootloaders in mobile devices,

    N. Redini, A. Machiry, D. Das, Y. Fratantonio, A. Bianchi, E. Gustafson, Y. Shoshitaishvili, C. Kruegel, and G. Vigna, “Boot- stomp: On the security of bootloaders in mobile devices,” in26th USENIX Security Symposium (USENIX Security 17), 2017, pp. 781– 798

    2017

  39. [39]

    {KSG}: Augmenting kernel fuzzing with system call specification generation,

    H. Sun, Y. Shen, J. Liu, Y. Xu, and Y. Jiang, “{KSG}: Augmenting kernel fuzzing with system call specification generation,” in2022 USENIX Annual Technical Conference (USENIX ATC 22), 2022, pp. 351–366

    2022

  40. [40]

    Binsec/se: A dynamic symbolic execution toolkit for binary-level analysis,

    R. David, S. Bardin, T. D. Ta, L. Mounier, J. Feist, M.-L. Potet, and J.-Y. Marion, “Binsec/se: A dynamic symbolic execution toolkit for binary-level analysis,” in2016 IEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering (SANER), vol. 1. IEEE, 2016, pp. 653–656

    2016

  41. [41]

    Linkrid: Vetting imbalance reference counting in linux kernel with symbolic execution,

    J. Liu, L. Yi, W. Chen, C. Song, Z. Qian, and Q. Yi, “Linkrid: Vetting imbalance reference counting in linux kernel with symbolic execution,” in31st USENIX Security Symposium (USENIX Security 22), 2022, pp. 125–142

    2022

  42. [42]

    Queryx: Symbolic query on decompiled code for finding bugs in cots binaries,

    H. Han, J. Kyea, Y. Jin, J. Kang, B. Pak, and I. Yun, “Queryx: Symbolic query on decompiled code for finding bugs in cots binaries,” in2023 IEEE Symposium on Security and Privacy (SP). IEEE, 2023, pp. 3279–3295

    2023

  43. [43]

    Fuzzusb: Hybrid stateful fuzzing of usb gadget stacks,

    K. Kim, T. Kim, E. Warraich, B. Lee, K. R. Butler, A. Bianchi, and D. J. Tian, “Fuzzusb: Hybrid stateful fuzzing of usb gadget stacks,” in2022 IEEE Symposium on Security and Privacy (SP). IEEE, 2022, pp. 2212–2229

    2022

  44. [44]

    Symjs: Automatic symbolic testing of javascript web applications,

    G. Li, E. Andreasen, and I. Ghosh, “Symjs: Automatic symbolic testing of javascript web applications,” inProceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2014, pp. 449–459

    2014

  45. [45]

    Automated exploit generation for node. js packages,

    F. Marques, M. Ferreira, A. Nascimento, M. E. Coimbra, N. Santos, L. Jia, and J. Fragoso Santos, “Automated exploit generation for node. js packages,”Proceedings of the ACM on Programming Languages, vol. 9, no. PLDI, pp. 1341–1366, 2025

    2025

  46. [46]

    ExpoSE: Practical symbolic execution of standalone javascript,

    B. Loring, D. Mitchell, and J. Kinder, “ExpoSE: Practical symbolic execution of standalone javascript,” inProceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 2017, pp. 196–199

    2017

  47. [47]

    Reach me if you can: On native vulnerability reachability in android apps,

    L. Borzacchiello, E. Coppa, D. Maiorca, A. Columbu, C. Demetrescu, and G. Giacinto, “Reach me if you can: On native vulnerability reachability in android apps,” inEuropean Symposium on Research in Computer Security. Springer, 2022, pp. 701–722

    2022

  48. [48]

    The domino effect: De- tecting and exploiting dom clobbering gadgets via concolic execution with symbolic dom,

    Z. Liu, T. Lee, J. Yu, Z. Kang, and Y. Cao, “The domino effect: De- tecting and exploiting dom clobbering gadgets via concolic execution with symbolic dom,” in34th USENIX Security Symposium (USENIX Security 25), 2025, pp. 8293–8312

    2025

  49. [49]

    Towards automatic detection and exploitation of java web applica- tion vulnerabilities via concolic execution guided by cross-thread object manipulation,

    X. Huang, L. Zhang, Y. Liu, P. Deng, Y. Cao, Y. Zhang, and M. Yang, “Towards automatic detection and exploitation of java web applica- tion vulnerabilities via concolic execution guided by cross-thread object manipulation,” in34th USENIX Security Symposium (USENIX Security 25), 2025, pp. 8367–8384

    2025

  50. [50]

    Finding bugs in dynamic web applications,

    S. Artzi, A. Kiezun, J. Dolby, F. Tip, D. Dig, A. Paradkar, and M. D. Ernst, “Finding bugs in dynamic web applications,” inProceedings of the 2008 international symposium on Software testing and analysis, 2008, pp. 261–272

    2008

  51. [51]

    Directed test generation for effective fault localization,

    S. Artzi, J. Dolby, F. Tip, and M. Pistoia, “Directed test generation for effective fault localization,” inProceedings of the 19th International Symposium on Software Testing and Analysis. Association for Computing Machinery, 2010, p. 49–60

    2010

  52. [52]

    Symbolic execution for javascript,

    J. F. Santos, P. Maksimović, T. Grohens, J. Dolby, and P. Gardner, “Symbolic execution for javascript,” inProceedings of the 20th In- ternational Symposium on Principles and Practice of Declarative Programming. Association for Computing Machinery, 2018

    2018

  53. [53]

    Testing android apps through symbolic execution,

    N. Mirzaei, S. Malek, C. S. Păsăreanu, N. Esfahani, and R. Mahmood, “Testing android apps through symbolic execution,”ACM SIGSOFT Software Engineering Notes, vol. 37, no. 6, pp. 1–5, 2012

    2012

  54. [54]

    Symqemu: Compilation-based sym- bolic execution for binaries,

    S. Poeplau and A. Francillon, “Symqemu: Compilation-based sym- bolic execution for binaries,” inNdss 2021, network and distributed system security symposium. Internet Society, 2021

    2021

  55. [55]

    Angr-the next generation of binary analysis,

    F. Wang and Y. Shoshitaishvili, “Angr-the next generation of binary analysis,” in2017 IEEE Cybersecurity Development (SecDev). IEEE, 2017, pp. 8–9

    2017

  56. [56]

    Unleashing mayhem on binary code,

    S. K. Cha, T. Avgerinos, A. Rebert, and D. Brumley, “Unleashing mayhem on binary code,” in2012 IEEE Symposium on Security and Privacy. IEEE, 2012, pp. 380–394

    2012

  57. [57]

    Symfit: Making the common (concrete) case fast for binary-code concolic execution,

    Z. Qi, J. Hu, Z. Xiao, and H. Yin, “Symfit: Making the common (concrete) case fast for binary-code concolic execution,” in33rd USENIX Security Symposium (USENIX Security 24), 2024, pp. 415– 432. 15

    2024

  58. [58]

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

    L.-A. Daniel, S. Bardin, and T. Rezk, “Binsec/rel: Efficient relational symbolic execution for constant-time at binary-level,” in2020 IEEE Symposium on Security and Privacy (SP). IEEE, 2020, pp. 1021– 1038

    2020

  59. [59]

    Practical verification of system-software components written in standard c,

    C. Cebeci,Y. Zou,D. Zhou,G. Candea,and C. Pit-Claudel,“Practical verification of system-software components written in standard c,” inProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, 2024, pp. 455–472

    2024

  60. [60]

    Automatically reasoning about how systems code uses the cpu cache,

    R. Iyer, K. Argyraki, and G. Candea, “Automatically reasoning about how systems code uses the cpu cache,” in18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24), 2024, pp. 581–598

    2024

  61. [61]

    Avatar: A framework to support dynamic security analysis of embedded systems’ firmwares

    J. Zaddach, L. Bruno, A. Francillon, D. Balzarottiet al., “Avatar: A framework to support dynamic security analysis of embedded systems’ firmwares.” inNDSS, vol. 14, no. 2014, 2014, pp. 1–16

    2014

  62. [62]

    Fie on firmware: Finding vulnerabilities in embedded systems using symbolic execu- tion,

    D. Davidson, B. Moench, T. Ristenpart, and S. Jha, “Fie on firmware: Finding vulnerabilities in embedded systems using symbolic execu- tion,” in22nd USENIX Security Symposium (USENIX Security 13), 2013, pp. 463–478

    2013

  63. [63]

    Fuzzware: Using pre- cise mmio modeling for effective firmware fuzzing,

    T. Scharnowski, N. Bars, M. Schloegel, E. Gustafson, M. Muench, G. Vigna, C. Kruegel, T. Holz, and A. Abbasi, “Fuzzware: Using pre- cise mmio modeling for effective firmware fuzzing,” in31st USENIX Security Symposium (USENIX Security 22), 2022, pp. 1239–1256

    2022

  64. [64]

    Co3: concolic co-execution for firmware,

    C. Liu, A. Mera, E. Kirda, M. Xu, and L. Lu, “Co3: concolic co-execution for firmware,” in33rd USENIX Security Symposium (USENIX Security 24), 2024, pp. 5591–5608

    2024

  65. [65]

    Patchverif: Discovering faulty patches in robotic vehicles,

    H. Kim,M. O. Ozmen,Z. B. Celik,A. Bianchi,andD. Xu,“Patchverif: Discovering faulty patches in robotic vehicles,” in32nd USENIX Security Symposium (USENIX Security 23), 2023, pp. 3011–3028

    2023

  66. [66]

    Symbolic pathfinder: symbolic execution of java bytecode,

    C. S. Păsăreanu and N. Rungta, “Symbolic pathfinder: symbolic execution of java bytecode,” inProceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering, 2010, pp. 179–180

    2010

  67. [67]

    Directedincremental symbolic execution,

    G. Yang,S. Person,N. Rungta,andS. Khurshid,“Directedincremental symbolic execution,”ACM Trans. Softw. Eng. Methodol., vol. 24, no. 1, 2014

    2014

  68. [68]

    Exact and approximate probabilistic symbolic execution for nondeter- ministic programs,

    K. Luckow, C. S. Păsăreanu, M. B. Dwyer, A. Filieri, and W. Visser, “Exact and approximate probabilistic symbolic execution for nondeter- ministic programs,” inProceedings of the 29th ACM/IEEE Interna- tional Conference on Automated Software Engineering. Association for Computing Machinery, 2014, p. 575–586

    2014

  69. [69]

    Automatically gen- erating test cases for safety-critical software via symbolic execution,

    E. Kurian, D. Briola, P. Braione, and G. Denaro, “Automatically gen- erating test cases for safety-critical software via symbolic execution,” Journal of Systems and Software, vol. 199, p. 111629, 2023

    2023

  70. [70]

    Reverse engineering and retrofitting robotic aerial vehicle control firmware using dispatch,

    T. Kim, A. Ding, S. Etigowni, P. Sun, J. Chen, L. Garcia, S. Zonouz, D. Xu, and D. Tian, “Reverse engineering and retrofitting robotic aerial vehicle control firmware using dispatch,” inProceedings of the 20th Annual International Conference on Mobile Systems, Appli- cations and Services, 2022, pp. 69–83

    2022

  71. [71]

    Symbolic execution for software testing: Three decades later,

    C. Cadar and K. Sen, “Symbolic execution for software testing: Three decades later,”Commun. ACM, vol. 56, no. 2, pp. 82–90, 2013

    2013

  72. [72]

    A survey of symbolic execution techniques,

    R. Baldoni, E. Coppa, D. C. D’elia, C. Demetrescu, and I. Finocchi, “A survey of symbolic execution techniques,”ACM Comput. Surv., vol. 51, no. 3, pp. 50:1–50:39, 2018

    2018

  73. [73]

    Compiling parallel symbolic execution with continuations,

    G. Wei, S. Jia, R. Gao, H. Deng, S. Tan, O. Bračevac, and T. Rompf, “Compiling parallel symbolic execution with continuations,” in2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). IEEE, 2023, pp. 1316–1328

    2023

  74. [74]

    Parallel symbolic execution for automated real-world software testing,

    S. Bucur, V. Ureche, C. Zamfir, and G. Candea, “Parallel symbolic execution for automated real-world software testing,” inProceedings of the sixth conference on Computer systems, 2011, pp. 183–198

    2011

  75. [75]

    Characteristic studies of loop problems for structural test generation via symbolic execution,

    X. Xiao, S. Li, T. Xie, and N. Tillmann, “Characteristic studies of loop problems for structural test generation via symbolic execution,” in2013 28th IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 2013, pp. 246–256

    2013

  76. [76]

    Symbolic arrays in symbolic pathfinder,

    A. Fromherz, K. S. Luckow, and C. S. Păsăreanu, “Symbolic arrays in symbolic pathfinder,”ACM SIGSOFT Software Engineering Notes, vol. 41, no. 6, pp. 1–5, 2017

    2017

  77. [77]

    Memory models in symbolic execution: key ideas and new thoughts,

    L. Borzacchiello, E. Coppa, D. Cono D’Elia, and C. Demetrescu, “Memory models in symbolic execution: key ideas and new thoughts,” Software Testing, Verification and Reliability, vol. 29, no. 8, p. e1722, 2019

    2019

  78. [78]

    Benchmarkingthecapability of symbolic execution tools with logic bombs,

    H.Xu,Z.Zhao,Y.Zhou,andM.R. Lyu,“Benchmarkingthecapability of symbolic execution tools with logic bombs,”IEEE Transactions on Dependable and Secure Computing, vol. 17, no. 6, pp. 1243–1256, 2020

    2020

  79. [79]

    Learning to accelerate symbolic execution via code transformation,

    J. Chen, W. Hu, L. Zhang, D. Hao, S. Khurshid, and L. Zhang, “Learning to accelerate symbolic execution via code transformation,” in32nd European Conference on Object-Oriented Programming (ECOOP 2018). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2018, pp. 6–1

    2018

  80. [80]

    When compileroptimiza- tions meet symbolic execution: An empirical study,

    Y. Zhang,M. Sirlanci,R. Wang,andZ. Lin,“When compileroptimiza- tions meet symbolic execution: An empirical study,” inProceedings of the 2024 on ACM SIGSAC Conference on Computer and Commu- nications Security, 2024, pp. 4212–4225

    2024

Showing first 80 references.