Source-linked AI summary
ATLAS: A Multi-Agent Framework for Lifting Binary to Canonical Compiler IR
Xiaoao Zhu, Ni Zhang, Jie Ren, Zhiqiang Li, Jie Zheng, Zhanyong Tang, Zheng Wang
TL;DR
Optimizations make it difficult to recover valid, behaviorally consistent canonical LLVM IR from stripped binaries, a representation useful for security analysis and migration. ATLAS combines structure-aware retrieval with multi-agent repair and validation; across evaluated datasets and architectures, it consistently improves lifting metrics over rule-based and LLM baselines.
Problem
Compiler optimizations alter control and data flow, eliminate variables, and introduce architecture-specific instruction sequences, making recovery of valid, behaviorally consistent canonical IR difficult.
Source: §I · p. 2, §II · p. 2Method
ATLAS combines retrieval-grounded IR synthesis with localized, diagnostic-driven repair and validation by separate agents.
Source: §I · p. 2Results
Across HumanEval-Decompile and MBPP, three ISAs, and optimization levels -O0 to -O3, ATLAS consistently improves recompilability, re-executability, and reference-IR similarity over rule-based and LLM baselines.
Source: §XV · p. 17Takeaways & Limitations
The lifted IR better supports SVF-based program analysis and cross-ISA software migration than the compared baselines.
Source: §XV · p. 17Behavioral evaluation benefits from curated unit tests, while real reverse-engineering settings rarely provide input–output oracles.
Source: §XIII · p. 16
Abstract
from arXiv · showhide
Lifting stripped, heavily optimized binaries to a canonical, pre-optimization LLVM intermediate representation (IR) is essential for downstream security analysis and legacy software migration when source code is unavailable. However, aggressive compiler optimizations rewrite control and data flow, remove structural metadata, and introduce type-erased low-level idioms, causing current lifters to produce malformed or semantically divergent IR. We present ATLAS, a multi-agent framework designed to reconstruct formally valid and canonical LLVM IR from optimized disassembly.ATLAS combines (i) Structure-aware, region-level retrieval, which utilizes pseudo-probe attribution to align optimized instructions with canonical IR exemplars, and (ii) a collaborative refinement loop that closes the gap between probabilistic generation and deterministic compiler constraints. Concretely, a Lift agent generates an initial IR draft conditioned on retrieved exemplars, an Advisor agent interprets LLVM verifier/compilation diagnostics and static checks to propose localized repair actions, and a Validation agent applies the edits, re-runs toolchain verification and (when available) runtime checks, and feeds the resulting diagnostics back to the Advisor. The agents iterate until the IR is verifier-clean and behaviorally consistent, or a budget limit is reached. On HumanEval-Decompile and MBPP, ATLAS outperforms seven baselines on lifting LLVM IR, achieving 91.8% re-executability and 89.4% CFG similarity across ARM, x86-64, and RISC-V binaries. Moreover, our evaluation demonstrates that ATLAS also outperforms the Binary to C to IR pipelines in pointer-flow precision and downstream analyzability. By recovering a well-formed, machine-centric representation, ATLAS enables practical cross-ISA recompilation and verifiable binary-only migration workflows.
I. INTRODUCTION
Binary recovery supports security analysis, legacy-system maintenance, and migration when source code is unavailable, but compiler optimization complicates reconstruction of control flow, data flow, and valid types. ATLAS combines structure-aware retrieval with multi-agent synthesis, repair, and validation to recover canonical LLVM IR.
I. INTRODUCTION
- Optimizations alter control and data flow, eliminate variables, and introduce architecture-specific instruction sequences, while LLM-generated IR can contain invalid types, inconsistent SSA definitions, or incorrect computations.Source: §I · p. 1
- On HumanEval-Decompile, ATLAS achieves 94.5% re-executability for x86-64 inputs, averaged across optimization levels, and 93.6% re-executability in x86-64-to-ARM64 migration.The evaluation also covers ARM64 and RISC-V binaries compiled at optimization levels -O0 through -O3.Source: §I · p. 2
- ATLAS separates lifting into initial synthesis, repair planning, and validation for optimized, stripped binaries targeting canonical LLVM IR.The framework builds on BRIDGE and further develops localized repairs, behavioral evidence when developer-written tests are unavailable, and cross-ISA reuse assessment.Source: §I · p. 2
- Structure-aware retrieval uses aligned assembly–IR exemplars across multiple ISAs, with LoRA adaptation of the assembly encoder for ARM64 and RISC-V.Source: §I · p. 2
- Localized repair maps diagnostics to affected IR slices and uses type, def–use, and control-flow constraints to guide targeted edits.A type or malformed-phi diagnostic may involve definitions, uses, and predecessor blocks beyond the reported line, so repairs must account for their dependencies together.Source: §I · p. 2
- Behavioral validation combines interface inference, dynamic observations, harness screening, and differential execution to guide repairs without developer-written tests.For accepted harnesses, ATLAS compares return values and observable memory effects on the same inputs for the original binary and recompiled IR.Source: §I · p. 2
II. MOTIVATION
The motivating task lifts an -O3 binary to canonical LLVM IR defined as the unoptimized output of a fixed clang -O0 configuration. Figure 2 contrasts six approaches, with RetDec distorting the original branch structure and general-purpose LLMs, especially Gemini-3 with RAG, preserving it more closely.
II. MOTIVATION
- The task reconstructs canonical LLVM IR from an -O3 optimized binary, with canonical defined as unoptimized LLVM IR emitted by a fixed clang -O0 configuration.Source: §II · p. 2
- Figure 2 compares six approaches, including RetDec, LLM Compiler FTD, ChatGPT-4o, Gemini-3, and RAG variants; Table I reports edit similarity, test-case pass, and branch recovery on x86-64.Source: §II · pp. 2–3, Table I · p. 3
- 38.2% edit similarity and PCI = 25 leave RetDec structurally misaligned despite passing available tests; Figure 2 shows its branch-to-select rewrite distorting if-else control flow.Source: Figure 2 · p. 3, §II · p. 3
- General-purpose LLMs, especially Gemini-3 with RAG, better preserve the CFG and produce IR closer to the canonical reference than the rule-based RetDec result.Source: Figure 2 · p. 3
LLVM IR
ATLAS targets canonical pre-optimization LLVM IR because executable lifts can still lose the original control-flow and data-flow structure needed by downstream analysis. Its retrieval-augmented results show improved structural similarity and analyzability, with the strongest reported recovery on Gemini-3.
LLVM IR
- LLM Compiler FTD and related approaches trained on compiler-emitted assembly face a different input domain from stripped raw-binary disassembly, which omits high-level cues.The paper notes that raw disassembly exposes indirect control flow and ABI-specific details.Source: LLVM IR · p. 4
- RAG raised ChatGPT-4o’s edit similarity from 32.0% to 65.0% and PCI from 18 to 32, although it did not fully recover the original branch-based CFG.The output retained a select-based formulation but used a more canonical stack-based -O0-style structure.Source: LLVM IR · p. 4
- 82.5% edit similarity, exact CFG matching, and PCI 39 were achieved by Gemini-3 with RAG, versus 26.0% edit similarity and PCI 21 without RAG.The RAG output also recovered the original if-else control-flow structure exactly.Source: LLVM IR · p. 4
- Executable or test-passing IR can remain structurally misaligned with canonical IR, motivating evaluation beyond compilability and test passing.ATLAS’s motivation identifies PCI and CFG-based metrics as relevant to downstream analyzability.Source: LLVM IR · p. 4
III. OVERVIEW
ATLAS combines three agents for lifting with a structure-aware retrieval database of aligned assembly and canonical LLVM IR. The database uses pseudo-probes to associate optimized machine-code regions with structurally coherent canonical IR slices.
III. OVERVIEW
- ATLAS’s LIFT, ADVISOR, and VALIDATION agents have distinct responsibilities in the pipeline for lifting optimized binaries to canonical pre-optimization LLVM IR.Canonical IR is defined as unoptimized IR emitted under a fixed clang -O0 toolchain configuration.Source: §III · p. 4
A. Offline RAG Database Preparation
- The offline database starts from ExeBench, removes near-duplicate functions above 0.95 normalized token-level edit similarity, and excludes evaluation-set overlaps.Retained sources are compiled at -O0 for canonical IR and at -O0 through -O3 for assembly; the resulting corpus contains 69,253 IR targets and 277,012 assembly–IR pairs.Source: A. Offline RAG Database Preparation · p. 5
B. Control-Flow-Aware Data Structuring
- Region-level entries pair assembly snippets with structurally coherent IR slices, creating tighter retrieval units than function-level pairs that bundle multiple control constructs.Each entry stores an assembly snippet, a canonical -O0 IR slice, and an identifier.Source: B. Control-Flow-Aware Data Structuring · p. 5
- AST-inserted PROBE anchors mark constructs such as conditionals and loops, and LLVM pseudo-probes attribute optimized machine-instruction ranges back to originating IR blocks.This attribution remains useful when optimization reorders instructions or basic blocks.Source: B. Control-Flow-Aware Data Structuring · p. 5
- The database extracts anchored canonical IR slices and corresponding region-complete assembly snippets, yielding 285K region-level entries.These region-level pairs are the retrieval units used at inference time.Source: B. Control-Flow-Aware Data Structuring · p. 5
C. Embedding and Indexing
The LIFT agent retrieves aligned exemplars for CFG-segmented assembly regions and uses them to generate an initial IR draft. Segmentation preserves local control structure, while retrieval quality is high under the paper’s canonical-region-label metric.
V. LIFT AGENT
- The LIFT agent disassembles binaries, recovers a coarse CFG, segments control-structure regions, retrieves aligned assembly–IR exemplars, and conditions an LLM to draft IR.The draft is passed to the ADVISOR agent for tool-guided refinement.Source: §V · p. 6
A. CFG-aligned Segmentation
- CFG segmentation starts regions at divergence blocks, follows successors, groups loop cycles, merges compatible loop fragments and converging branches, and falls back to address ranges when CFG recovery is incomplete.External stubs and unresolved callees are filtered before segmenting the target function’s internal control flow.Source: A. CFG-aligned Segmentation · p. 6
C. Embedding and Indexing
- Nova-1.3B embeds each segmented assembly region for nearest-neighbor search over a FAISS index of aligned exemplars.The retrieved assembly–IR pairs provide in-context evidence for IR synthesis.Source: B. Control-flow-aware Retrieval · p. 6
B. Control-flow-aware Retrieval
- 95.92%, 98.61%, and 98.83% Top-1, Top-3, and Top-5 retrieval accuracy were achieved by Nova-1.3B, respectively.Accuracy is the fraction of queries with at least one retrieved exemplar sharing the query’s canonical region label.Source: B. Control-flow-aware Retrieval · p. 6
C. Initial IR Synthesis
Initial IR synthesis uses retrieved exemplars, then the ADVISOR localizes failures and proposes scoped repairs. VALIDATION applies edits and iterates compilation and available runtime checks, stopping on success or at a five-iteration cap.
C. Initial IR Synthesis
- The initial IR draft is prompted with the query assembly region and top-ranked retrieved assembly–IR exemplars, retaining the full query region within a fixed context budget.The prompt requests a single-function LLVM IR draft in canonical, pre-optimized style.Source: C. Initial IR Synthesis · p. 6
VI. ADVISOR AGENT
- The ADVISOR maps compiler, verifier, and available runtime failures to localized IR scopes, then proposes minimal repair actions such as type fixes, CFG updates, declarations, or targeted rewrites.Failure categories constrain repair prompts and reduce prompt noise.Source: §VI · pp. 6–7
- Specialized repairs use failing-test evidence for behavioral mismatches, binary interface facts for linkage or ABI mismatches, predecessor constraints for phi errors, and def–use slices for definition conflicts.These category-specific contexts guide targeted edits to the relevant IR slice.Source: §VI · p. 7
VII. VALIDATION AGENT
- VALIDATION applies edits, reruns LLVM compilation and verification, and executes assertion-based tests after compilation succeeds, returning diagnostics and behavioral evidence for further repair.The agents stop when toolchain verification and all available tests pass, or after five repair iterations.Source: §VII · p. 7
VIII. EXPERIMENTAL SETUP
The evaluation compares ATLAS with rule-based lifters and general-purpose LLMs on two compiled-binary benchmarks, using measures of toolchain validity, behavior, and structural fidelity.
A. Competitive Baselines
- ATLAS is compared with RetDec and MCTOLL, plus five general-purpose LLMs; MCTOLL supports only x86-64.API-based LLM baselines are each run five times with the same prompt, and results are averaged.Source: A. Competitive Baselines · p. 7
B. Evaluation Datasets
- HumanEval-Decompile contains 164 programs with executable tests, while the evaluation selects 500 consistently compilable and executable MBPP programs.Both benchmarks use canonical LLVM IR generated with fixed Clang 19 -O0 settings; binaries are compiled from -O0 through -O3 and disassembled with llvm-objdump.Source: B. Evaluation Datasets · p. 7
C. Metrics
- Five metrics assess recompilability, re-executability, edit similarity, CFG full-match accuracy, and CFG similarity.Together, they measure toolchain validity, behavioral correctness, and structural fidelity to the canonical reference IR.Source: C. Metrics · p. 8
- Recompilability measures successful assembly and compilation, whereas re-executability additionally requires passing the associated tests.The re-executability test reflects consistency with the reference program under available inputs.Source: C. Metrics · p. 8
- Edit similarity uses normalized edit distance, while CFG full-match tests graph isomorphism and CFG similarity uses the Weisfeiler–Lehman graph kernel.Higher edit similarity and CFG similarity indicate closer agreement with the reference; full-match requires exactly isomorphic CFGs.Source: C. Metrics · p. 8
IX. EXPERIMENTAL RESULTS
ATLAS achieves stronger lifting results across architectures and benchmarks, while CFG-level retrieval offers the strongest overall balance among the tested retrieval granularities. The results also show that whole-function retrieval is less robust under heavier optimization.
A. Overall Performance
- 94.5% on x86-64, 94.2% on ARM64, and 80.6% on RISC-V re-executability for HumanEval-Decompile; the strongest non-ATLAS baselines remain below 30% on ARM64 and RISC-V.Averaged over -O0–-O3, ATLAS has the highest re-executability in nearly all reported settings.Source: A. Overall Performance · p. 9
- RetDec reaches 92.5% recompilability but 45.3% re-executability on HumanEval-Decompile x86-64, illustrating the gap between compiling and preserving behavior.On ARM64, RetDec reaches 92.8% recompilability and 0.5% re-executability; the passage reports a similar gap on MBPP.Source: A. Overall Performance · p. 9
- 51.0% on x86-64, 44.3% on ARM64, and 51.8% on RISC-V edit similarity for ATLAS on HumanEval-Decompile, exceeding the corresponding baselines.The same improvement trend holds on MBPP alongside substantially higher re-executability.Source: A. Overall Performance · p. 9
- 26.9%, 18.3%, and 20.1% CFG full-match accuracy, and 97.8, 84.1, and 90.2 CFG similarity for ATLAS on x86-64, ARM64, and RISC-V, respectively.All baselines remain below 6% full-match accuracy; on RISC-V, high similarity coexists with lower exact-match recovery.Source: Figure 7 · p. 9, A. Overall Performance · p. 9
B. Multi-Level RAG in Lift Agent
- 87.8% average recompilability, 56.9% average re-executability, and 51.0% average edit similarity make control-flow retrieval the strongest overall balance.Compared with basic-block retrieval, it improves average recompilability by 19.4 points and re-executability by 7.7 points.Source: B. Multi-Level RAG in Lift Agent · p. 9, Table IV · p. 10
- At -O3, control-flow retrieval reaches 90.2% recompilability and 55.5% re-executability, while basic-block retrieval reaches 53.2% and 40.2%, respectively.Function-level retrieval improves on basic-block retrieval but degrades at higher optimization levels and does not outperform control-flow retrieval overall.Source: B. Multi-Level RAG in Lift Agent · p. 10
C. Ablation: Impact of the Advisor–Validation Refinement Loop
The refinement loop substantially improves recompilability and re-executability, while edit similarity stays nearly unchanged. ATLAS also shows downstream pointer-analysis and cross-ISA migration results on the stated benchmarks and configurations.
C. Ablation: Impact of the Advisor–Validation Refinement Loop
- 99.2% recompilability and 94.5% re-executability with the refinement loop, up from 87.8% and 56.9% in the Lift-only setting.The gains are consistent across optimization levels and particularly large at -O1–-O3.Source: C. Ablation: Impact of the… · p. 10
- 51.0% versus 51.4% edit similarity with and without refinement, suggesting that the loop primarily makes localized, diagnostic-driven repairs.The passage characterizes retrieval-grounded initial synthesis as a strong starting point and tool-guided refinement as the main driver of end-to-end correctness.Source: C. Ablation: Impact of the… · p. 10
X. DOWNSTREAM ANALYZABILITY
- ATLAS reaches PCI 132.9, compared with 80.4 for LLM4Decompile+clang and 107.1 for RetDec, in the SVF-based analysis evaluation.Its average alias set size is 1.00; the passage says the results indicate better preservation of analysis-relevant typing and memory-flow information.Source: Table VI · p. 11, §X · p. 11
XI. DOWNSTREAM CROSS-ISA MIGRATION
- For x86-64-to-ARM64 migration, ATLAS achieves 98.3% recompilability and 93.6% re-executability, versus RetDec's 90.6% and 44.1%.LLM4Decompile reaches 82.5% recompilability and 40.7% re-executability in the same comparison.Source: Table VII · p. 11, §XI · p. 11
- ATLAS exceeds 97% recompilability across all reported source–target pairs, with its best reported cross-ISA re-executability at 93.6% for x86-64 to ARM64 or RISC-V.The passages describe strong transfer performance from ARM64 and RISC-V as well.Source: Table VIII · p. 11, Table IX · p. 11, §XI · p. 11
XII. FURTHER ANALYSIS
ATLAS improves lifting metrics across five general-purpose LLM backbones. The reported gains span backbones and optimization levels, rather than relying on one model.
A. Generalization Across Backbone LLMs
- 70.7% recompilability, 54.3% re-executability, and 46.4% edit similarity averaged across five backbones with ATLAS, versus 24.4%, 13.0%, and 30.3% for the base models.The passage reports improvement on all three primary lifting metrics for every backbone.Source: A. Generalization Across Backbone LLMs · p. 12
- For Gemini-3, ATLAS raises average recompilability from 45.7% to 99.2% and re-executability from 30.2% to 94.5%.For DeepSeek-V3.2, it raises those metrics from 28.4% to 88.2% and from 10.1% to 68.2%, respectively.Source: A. Generalization Across Backbone LLMs · p. 12
- At -O3, Qwen-Plus with ATLAS reaches 50.0% recompilability and 37.9% re-executability, compared with 6.8% and 3.4% for the base model.Across -O0 to -O3, ATLAS maintains 98.8–100.0% recompilability and 93.9–96.1% re-executability.Source: A. Generalization Across Backbone LLMs · p. 12
- The figure traces one HumanEval-Decompile case through five refinement cycles toward the ground-truth embedding.The latent embeddings are projected with IR2vector [26].Source: Figure 8 · p. 12
B. Lifting Direction Correction
ATLAS’s refinement moves lifted IR toward the canonical reference, with larger gains in execution and compilability than in textual similarity. Performance remains strong on many longer functions, though the longest inputs expose behavioral and textual-fidelity challenges.
C. Impact of iterative refinement.
- Refinement raises re-executability from 56.9% at k = 0 to 94.5% at k = 5 and re-compilability from 87.8% to 99.2%, while edit similarity changes from 50.9% to 51.4%.Beyond k = 5, re-executability rises only to 95.0% at k = 7, and re-compilability drops slightly; the authors set k = 5 as the default budget.Source: Table XI · p. 13, C. Impact of iterative refinement · p. 13
B. Lifting Direction Correction
- Refinement trajectories move toward the ground-truth IR in steps, typically reaching its neighborhood in one iteration for -O0 inputs and requiring multiple iterations for -O1–-O3 inputs.The t-SNE visualization is qualitative and does not establish semantic equivalence.Source: B. Lifting Direction Correction · pp. 12–13
D. Impact of Input Length on Decompilation Performance
- For inputs of 140–395 instructions, ATLAS retains 100% Re-compilability and 93.8% CFG Similarity, while Re-executability falls to 73.1%.For [60, 80] instructions, ATLAS achieves 100% re-executability; general-purpose LLM re-executability falls below 9% beyond 60 instructions, except Gemini-3 at 31.0%.Source: D. Impact of Input Length on… · p. 13, Figure 10 · p. 14
- In the [2] instruction range, ATLAS achieves near-perfect Re-executability despite 28.6% CFG Similarity and 49.0% Edit Similarity.The authors attribute low similarity scores in small functions to the disproportionate effect of register names, function attributes, and entry/exit blocks.Source: D. Impact of Input Length on… · pp. 13–14
- For -O1 and -O3 inputs, re-executability declines in the 140+ instruction long tail, while average edit similarity is 64.3% for -O0 and decreases in the long-tail regime.The long-tail regime accounts for 54.2% of HumanEval-Decompile.Source: D. Impact of Input Length on… · p. 13, Figure 11 · p. 14
- On functions with more than 200 instructions, ATLAS reaches 100% re-compilability, 76.9% re-executability, and 44.4% edit similarity, versus RetDec’s 91.1%, 10.7%, and 23.9%.The comparison covers 56 long cases from HumanEval and MBPP.Source: Table XII · p. 15, D. Impact of Input Length on… · p. 15
E. Error Types Considered in ATLAS
The refinement loop reduces compilation and verification failures, while runtime tests help resolve remaining behavioral errors. Human-written tests yield higher re-executability than structural-only feedback or LLM-generated tests.
E. Error Types Considered in ATLAS
- By the fifth refinement iteration, total failures drop by 81.2%, with remaining failures dominated by AssertError after compiler- and verifier-reported issues are reduced.FuncNameError falls from 110 under one-shot inference to 22 by the third pass; PhiError and DefinitionConflict also decline.Source: E. Error Types Considered in ATLAS · p. 15
F. Impact of Test-Case–Guided Feedback
- Re-executability is 88.0% without tests, 89.5% with LLM-generated tests, and 94.5% with human-written tests; re-compilability remains 98.6–99.2% across settings.Edit similarity remains essentially unchanged at 51.2–51.4%.Source: F. Impact of Test-Case–Guided Feedback · pp. 15–16
G. Cost Analysis of ATLAS
ATLAS’s full five-round refinement configuration has a reported average cost of $0.0446 per function, while the authors identify architecture extension and very large inputs as practical boundaries. The conclusion presents ATLAS as supporting analysis and cross-ISA migration through analysis-ready LLVM IR.
G. Cost Analysis of ATLAS
- A six-session run averages 19,573 input tokens and 11,610 output tokens, costing $0.0446 per function with the Gemini-3 backbone.This is an upper-bound configuration under a fixed five-round refinement budget; many functions converge in fewer iterations.Source: G. Cost Analysis of ATLAS · p. 16
XIII. DISCUSSION AND LIMITATIONS
- Extending ATLAS to additional architectures requires rebuilding the structure-aware RAG database, and cross-ISA transfer is not guaranteed without reindexing and calibration.The data-construction pipeline can be rerun with the appropriate compiler backend and instrumentation settings.Source: §XIII · p. 16
- Very large or highly entangled functions may exceed the model context window and require further decomposition and interface contracts to stitch regions together.The current design mitigates input length by segmenting code into CFG-aligned regions.Source: §XIII · p. 16
A. LLVM Intermediate Representations Recovery
- Prior binary-to-LLVM IR tools are described as struggling with SSA reconstruction, control-flow preservation, or semantic fidelity under aggressive optimization; ATLAS uses control-flow-aware retrieval and pseudo-probe instrumentation.The passage discusses McSema, LLVM-MCTOLL, RevGen, Schwartz et al., and LeanBin.Source: A. LLVM Intermediate Representations… · p. 16
B. Learning-Based and Neural Decompilation Methods
- ATLAS targets raw-binary LLVM IR lifting, whereas LLM Compiler FTD and Forklift use metadata from compiler-emitted assembly unavailable in raw binaries.The passage contrasts LLVM IR’s precise typing and structural-fidelity demands with binary-to-C decompilation.Source: B. Learning-Based and Neural… · p. 17
C. Retrieval-Augmented Generation in Code Tasks
- Existing RAG methods discussed target high-level code synthesis or binary tasks without IR-specific structural constraints; ATLAS uses fine-grained, control-flow-aware retrieval for binary-to-LLVM IR lifting.The passage names CodeRAG, BTR, R2AG, and LI-RAGE among related methods.Source: C. Retrieval-Augmented Generation in… · p. 17
XV. CONCLUSION
- Across HumanEval-Decompile and MBPP, three ISAs, and optimization levels -O0 to -O3, ATLAS improves recompilability, re-executability, and reference-IR similarity over rule-based and LLM-based baselines.The conclusion also reports downstream use in SVF-based analysis and cross-ISA software migration.Source: §XV · p. 17