Program Synthesis for Exploit Generation

Abstract

We formalize the problem of generating working exploits from vulnerability findings as a syntax-guided synthesis (SyGuS) problem. Given a domain-specific grammar of exploit primitives—flash loan operations, token swaps, contract calls, state assertions—and a specification expressed as pre/post-conditions over blockchain state, the task is to synthesize a program (a transaction sequence) that satisfies the specification. The specification is simple: the precondition asserts a vulnerability exists in the target contract; the postcondition asserts the attacker’s balance has increased. We define the exploit grammar formally, show that fork-based EVM execution serves as a sound correctness oracle, and adapt counter-example guided inductive synthesis (CEGIS) to the exploit domain. We demonstrate that static analysis findings from vulnerability detectors act as synthesis constraints that prune the search space by orders of magnitude, reducing the problem from intractable enumeration to targeted template instantiation. The framework unifies ad-hoc exploit generation techniques under a single formal model and provides correctness guarantees: any synthesized exploit that executes successfully on a forked chain is a constructive proof that the vulnerability is real.

1. Introduction

Vulnerability detection and exploit generation are distinct problems. A static analyzer that flags a reentrancy pattern has identified a necessary condition for an attack—an unsafe ordering of external calls and state updates—but has not demonstrated that the condition is sufficient. The gap between “this pattern exists” and “this contract can be drained” is where false positives live. Closing that gap requires constructing a concrete attack: a sequence of transactions with specific calldata, value transfers, and contract deployments that, when executed against real chain state, transfers funds from the victim to the attacker.

This construction problem is a program synthesis problem. The attacker must produce a program (the exploit) that meets a specification (profit extraction) using a restricted set of operations (blockchain transactions). The program operates over a well-defined state model (EVM world state), and correctness can be verified mechanically by executing the candidate on a forked chain.

Program synthesis is a mature field in programming languages research. The syntax-guided synthesis (SyGuS) framework [Alur et al., 2013] provides a standard formulation: given a background theory, a grammar defining the space of candidate programs, and a specification, find a program in the grammar that satisfies the specification. Counter-example guided inductive synthesis (CEGIS) [Solar-Lezama et al., 2006] provides an efficient search strategy: propose a candidate, check it against the specification, and if it fails, use the failure as a counter-example to guide the next proposal.

This paper applies these ideas to exploit generation. We define:

1. A grammar of exploit primitives and their composition rules
2. A specification language over blockchain state transitions
3. A correctness oracle based on fork-mode EVM execution
4. A CEGIS-based search that iteratively refines exploit candidates
5. A pruning strategy that uses static analysis findings to constrain the grammar

The result is a framework where exploit generation is not an ad-hoc script-writing exercise but a formal synthesis problem with well-defined completeness and soundness properties.

2. Preliminaries

2.1 Syntax-Guided Synthesis

The SyGuS framework [Alur et al., 2013] formulates synthesis as follows. Let L be a background logic (e.g., linear arithmetic, bit-vectors). A SyGuS problem is a tuple (G, phi) where:

• G is a context-free grammar defining the syntactic search space
• phi(f, x) is a specification: a formula in L that the synthesized function f must satisfy for all inputs x

The solver must find a function f expressible by G such that for all x, phi(f, x) holds. The grammar constrains the search space, and the specification defines correctness.

2.2 Counter-Example Guided Inductive Synthesis

CEGIS [Solar-Lezama et al., 2006] decomposes the synthesis problem into two interacting phases:

1. Synthesis phase: Given a finite set of input-output examples E, find a program p in G that is consistent with all examples in E.
2. Verification phase: Check whether p satisfies phi for all inputs. If yes, return p. If no, produce a counter-example c where p fails, add c to E, and return to phase 1.

The key insight is that synthesis over finitely many examples is easier than synthesis over a universal specification. The verifier progressively strengthens the example set until the synthesized program is correct.

2.3 Blockchain State Model

We model the blockchain as a state machine. Let sigma denote the world state: a mapping from addresses to account states, where each account state includes balance, nonce, code, and storage. A transaction tx is a function sigma -> sigma’ that transforms the world state. A transaction sequence T = [tx_1, …, tx_n] composes sequentially: sigma_n = tx_n(… tx_1(sigma_0) …). The state is deterministic given the starting state and transaction sequence.

We write sigma.bal(a) for the ETH balance of address a in state sigma, and sigma.store(a, s) for storage slot s of contract a.

3. The Exploit Synthesis Problem

3.1 Formal Problem Statement

An exploit synthesis problem is a tuple (G_E, sigma_0, phi_pre, phi_post, O) where:

• G_E is an exploit grammar (Section 4)
• sigma_0 is the initial world state (obtained from a chain fork at a specific block)
• phi_pre(sigma_0) is a precondition asserting the vulnerability exists
• phi_post(sigma_0, sigma_n, a_atk) is a postcondition, typically: sigma_n.bal(a_atk) > sigma_0.bal(a_atk)
• O is a correctness oracle: a function that executes a candidate exploit against sigma_0 and returns the resulting state sigma_n or an execution failure

The synthesis task is to find a transaction sequence T expressible by G_E such that phi_post(sigma_0, O(T, sigma_0), a_atk) holds.

3.2 The Soundness Property

A synthesized exploit is a constructive proof of vulnerability. If a candidate program T executes on a fork of mainnet state and the postcondition holds (attacker balance increased), then the vulnerability is real and exploitable at that block height. This eliminates an entire class of false positives: any finding that cannot be converted to a working exploit (within the grammar and search budget) remains unconfirmed.

Formally: if O(T, sigma_0) = sigma_n and phi_post(sigma_0, sigma_n, a_atk) holds, then the vulnerability that phi_pre describes is exploitable. The converse does not hold—failure to synthesize does not prove safety, as the grammar or search budget may be insufficient.

4. Exploit Grammar

We define a domain-specific language (DSL) for exploit programs as a context-free grammar.

4.1 Grammar Definition

Exploit     ::= Setup TxSeq Teardown
Setup       ::= DeployAtk | epsilon
TxSeq       ::= Tx | Tx ';' TxSeq
Tx          ::= FlashLoan | Swap | Call | SelfCall | Assert | Block
FlashLoan   ::= 'flash' Provider Amount Body 'repay'
Swap        ::= 'swap' DEX TokenIn TokenOut Amount
Call        ::= 'call' Address Function Args Value
SelfCall    ::= 'selfcall' Function Args
Assert      ::= 'assert' Condition
Block       ::= 'advanceBlock' TxSeq
DeployAtk   ::= 'deploy' ContractTemplate
Body        ::= TxSeq
Provider    ::= 'aave_v3' | 'balancer' | 'uniswap_v3' | 'maker'
Amount      ::= Literal | 'max' | 'balance_of' Address Token
ContractTemplate ::= 'reentrancy_atk' | 'delegatecall_atk' | 'callback_atk' | 'generic_atk'

4.2 Primitive Semantics

Each production has a well-defined state transformer semantics:

Primitive	State Transformation
flash Provider Amount Body repay	Borrow Amount from Provider, execute Body, repay. Reverts if repayment fails.
swap DEX TokenIn TokenOut Amount	Exchange Amount of TokenIn for TokenOut via DEX router.
call Address Function Args Value	Send transaction to Address calling Function with Args and Value wei.
advanceBlock TxSeq	Simulate a block boundary, then execute TxSeq in the next block context.
deploy ContractTemplate	Deploy an attacker contract from a parameterized template.

4.3 Search Space Size

The grammar is finite-depth but the combinatorial explosion is severe. For a contract with f public functions, d DEX pools, and p flash loan providers, a single-transaction exploit of depth k (number of nested operations) has O((f + d + p)^k) candidates. A multi-transaction exploit of length n multiplies this by the sequence dimension: O(((f + d + p)^k)^n).

Without pruning, even modest parameters (f = 20, d = 5, p = 4, k = 4, n = 3) yield approximately 10^{15} candidates. Exhaustive enumeration is infeasible.

5. Specification and Correctness

5.1 Preconditions

The precondition phi_pre encodes the vulnerability finding from static analysis. For each vulnerability class, we define a predicate:

• Reentrancy: There exists a function f in the target contract where an external call precedes a state update to storage slot s, and f is reachable from a public entry point.
• Access control: There exists a privileged function f (one that modifies critical state) callable by an arbitrary address.
• Oracle manipulation: The contract reads a price from a source p that can be influenced by a single transaction (e.g., a spot price from a low-liquidity pool).
• Integer overflow: An arithmetic operation in function f can produce a value outside the representable range given attacker-controlled inputs.

These preconditions are discharged by the static analyzer before synthesis begins. They are not checked during synthesis—they serve to justify that a solution exists.

5.2 Postconditions

The postcondition phi_post defines what constitutes a successful exploit. The primary postcondition is profit:

phi_post(sigma_0, sigma_n, a_atk) :=
    sigma_n.bal(a_atk) > sigma_0.bal(a_atk) + gas_cost(T)

This can be generalized to token-denominated profit:

phi_post_token(sigma_0, sigma_n, a_atk, token) :=
    sigma_n.store(token, balanceOf[a_atk]) > sigma_0.store(token, balanceOf[a_atk])

Secondary postconditions capture severity: the magnitude of the profit, whether it drains the entire contract, or whether it requires specific preconditions (e.g., a governance timelock delay).

5.3 The Execution Oracle

The oracle O is a fork-mode EVM execution environment (e.g., Anvil, Hardhat Network, or a custom EVM interpreter). Given a candidate exploit T and initial state sigma_0 (forked from mainnet at a target block), O executes T and returns one of:

• Success(sigma_n): The exploit completed without revert. The resulting state is available for postcondition checking.
• Revert(reason): A transaction in T reverted. The reason string provides diagnostic information for search refinement.
• OutOfGas: The exploit exceeded the block gas limit.

The oracle is sound: if it reports success and the postcondition holds, the exploit is valid at that block height. It is not complete—the oracle only checks concrete executions, not symbolic ones—but for exploit generation, concrete soundness is the relevant property.

flowchart TD
    classDef process fill:#1a2233,stroke:#7ea8d4,stroke-width:2px,color:#c0d8f0
    classDef data fill:#332a1a,stroke:#d4b870,stroke-width:2px,color:#f0e0c0
    classDef success fill:#1a331a,stroke:#a8c686,stroke-width:2px,color:#c8e8b0
    classDef attack fill:#331a1a,stroke:#d97777,stroke-width:2px,color:#f0c0c0
    classDef highlight fill:#332519,stroke:#e8a87c,stroke-width:2px,color:#f0d8c0

    C["Candidate Exploit T"]:::attack
    F["Fork-Mode EVM\n(Anvil / Hardhat)"]:::process
    S["sigma_0\n(Mainnet State at Block N)"]:::data
    E["Execute T against sigma_0"]:::process
    R{"Revert?"}:::highlight
    SN["sigma_n\n(Resulting State)"]:::data
    PC{"phi_post holds?"}:::highlight
    OK["Valid Exploit"]:::success
    FAIL["Refine / Reject"]:::attack

    C --> E
    S --> F --> E
    E --> R
    R -- "No" --> SN --> PC
    R -- "Yes" --> FAIL
    PC -- "Yes" --> OK
    PC -- "No" --> FAIL

6. Search Strategies

6.1 Enumerative Synthesis

The simplest strategy enumerates programs in the grammar in order of increasing size (number of AST nodes). For each candidate, the oracle evaluates it and checks the postcondition. This is complete—it will find an exploit if one exists within the grammar—but impractically slow for large search spaces.

Algorithm 1: Enumerative Exploit Synthesis

function ENUMERATE(G_E, sigma_0, phi_post, max_depth):
    for depth = 1 to max_depth:
        for T in programs(G_E, depth):
            result = O(T, sigma_0)
            if result = Success(sigma_n) and phi_post(sigma_0, sigma_n):
                return T
    return FAILURE

The practical search space makes this approach viable only for exploits of depth 2-3 with a constrained grammar.

6.2 Template-Guided Synthesis

Template-guided synthesis replaces open-ended enumeration with parameterized templates that contain “holes” to be filled. A template captures the high-level structure of an exploit class; synthesis fills in concrete values.

For example, a reentrancy exploit template:

T_reentrancy := deploy(reentrancy_atk[?callback, ?target_fn])
              ; call(?target, ?target_fn, ?args, ?value)

Here ?callback, ?target_fn, ?args, and ?value are holes. The search space is reduced from the full grammar to the Cartesian product of hole domains:

• ?target_fn ranges over functions that the static analyzer flagged as reentrant
• ?callback ranges over functions callable on the victim during the callback
• ?args ranges over concrete argument values (determined by constraint solving or fuzzing)
• ?value ranges over ETH amounts (from 0 to the attacker’s available balance)

This reduces the search from O((f + d + p)^k) to O(|flagged_fns| * |callback_fns| * |arg_space|), which is typically manageable.

6.3 CEGIS for Exploit Synthesis

We adapt the CEGIS loop to the exploit domain. The key adaptation is that the “counter-example” is not a failing input but a diagnostic from a failing execution: a revert reason, an insufficient balance, or a failed assertion.

Algorithm 2: CEGIS Exploit Synthesis

function CEGIS_EXPLOIT(G_E, sigma_0, phi_post, findings):
    constraints = INITIAL_CONSTRAINTS(findings)
    examples = {}

    loop:
        // Synthesis phase: find candidate consistent with constraints
        T = SYNTHESIZE(G_E, constraints, examples)
        if T = FAILURE:
            return NO_EXPLOIT_FOUND

        // Verification phase: execute and check
        result = O(T, sigma_0)

        if result = Success(sigma_n) and phi_post(sigma_0, sigma_n):
            return T  // Exploit found

        // Extract diagnostic and refine
        diag = DIAGNOSE(result, T)
        constraints = REFINE(constraints, diag)
        examples = examples + {diag}

The DIAGNOSE function extracts structured information from execution failures:

Failure Mode	Diagnostic	Constraint Update
Revert at CALL to target	Function selector rejected	Remove selector from candidate space
Revert “insufficient balance”	Flash loan amount too small	Increase minimum loan amount
Revert “reentrancy guard”	Target has mutex lock	Switch to cross-function template
Success but no profit	Postcondition fails	Adjust extraction mechanism
OutOfGas	Exploit too deep	Reduce nesting depth

Each iteration narrows the search space. In practice, most exploits for known vulnerability classes converge within 5-15 iterations of the CEGIS loop, because the diagnostic information is highly informative.

flowchart TD
    classDef process fill:#1a2233,stroke:#7ea8d4,stroke-width:2px,color:#c0d8f0
    classDef data fill:#332a1a,stroke:#d4b870,stroke-width:2px,color:#f0e0c0
    classDef success fill:#1a331a,stroke:#a8c686,stroke-width:2px,color:#c8e8b0
    classDef attack fill:#331a1a,stroke:#d97777,stroke-width:2px,color:#f0c0c0
    classDef highlight fill:#332519,stroke:#e8a87c,stroke-width:2px,color:#f0d8c0

    INIT["Initialize Constraints\nfrom Static Findings"]:::data
    SYN["Synthesize Candidate T\nfrom Grammar + Constraints"]:::process
    EXEC["Execute T on Fork"]:::process
    CHECK{"Success +\nphi_post?"}:::highlight
    DIAG["Diagnose Failure\nExtract Counter-Example"]:::attack
    REFINE["Refine Constraints\nNarrow Search Space"]:::process
    DONE["Return Exploit T"]:::success
    FAIL["No Exploit\n(Budget Exhausted)"]:::attack

    INIT --> SYN
    SYN --> EXEC --> CHECK
    CHECK -- "Yes" --> DONE
    CHECK -- "No" --> DIAG --> REFINE --> SYN
    SYN -- "No candidates" --> FAIL

7. Finding-Guided Pruning

The central practical contribution of this framework is that static analysis findings dramatically constrain the synthesis problem. Without findings, the synthesizer must search the full grammar. With findings, the search is guided to a narrow region of the program space.

7.1 Findings as Grammar Restrictions

Each vulnerability class maps to a restricted sub-grammar:

Finding Type	Grammar Restriction	Effect
Reentrancy on function f	Fix template to reentrancy_atk, fix target to f	Eliminates all non-reentrancy templates
Access control on f	Fix template to generic_atk, fix entry to f	No flash loan or swap needed
Oracle manipulation via pool p	Require swap on p before call	Constrains transaction ordering
Flash loan profitability	Require flash wrapper	Adds flash loan structure

7.2 Formal Pruning

Let |G_E|_d denote the number of programs of depth at most d in grammar G_E. A finding F induces a restricted grammar G_E|_F by eliminating productions incompatible with the finding. The pruning ratio is:

rho(F) = |G_E|_F|_d / |G_E|_d

For typical vulnerability findings, empirical measurements show:

• Reentrancy finding: rho ~ 10^{-4} (reduces search space by 4 orders of magnitude)
• Access control finding: rho ~ 10^{-6} (the exploit structure is almost fully determined)
• Oracle manipulation: rho ~ 10^{-3} (constrained by the specific price source)

These reductions transform the problem from intractable enumeration to feasible search, typically completing within seconds rather than hours.

7.3 Multiple Findings

When multiple findings exist for the same contract, they can be synthesized independently (yielding multiple exploits) or composed. Composition introduces additional complexity: two individually exploitable vulnerabilities may enable a combined attack more severe than either alone. The grammar supports composition by allowing exploit programs to reference intermediate state produced by earlier transactions.

8. Multi-Transaction Synthesis

8.1 The Sequence Dimension

Many real-world exploits require multiple transactions across block boundaries. Oracle manipulation attacks are the canonical example: the attacker must first manipulate a price (transaction 1, block N), wait for a time-weighted average to update (block N+k), then exploit the stale price (transaction 2, block N+k). The grammar’s advanceBlock production handles this, but it adds a dimension to the search: the number of transactions and the block gaps between them.

8.2 Extended Grammar

Multi-transaction synthesis extends the grammar with block-boundary-aware sequencing:

MultiExploit  ::= Phase | Phase '|block|' MultiExploit
Phase         ::= TxSeq

The |block| separator denotes a block boundary. State persists across boundaries, but block-dependent values (block number, timestamp, TWAP accumulator) advance. The oracle must simulate block production to handle these semantics correctly—advancing timestamps, updating accumulators, and processing any pending transactions from other actors.

8.3 Search Complexity

The multi-transaction search space grows multiplicatively. For n phases with individual search spaces S_1, …, S_n, the combined space is S_1 * … * S_n * B where B is the set of possible block gap configurations. In practice, n rarely exceeds 3 and B is constrained by the vulnerability semantics (e.g., a TWAP manipulation requires at least w blocks where w is the observation window). Template-guided synthesis reduces this further by fixing n and the block gap structure based on the finding type.

flowchart LR
    classDef process fill:#1a2233,stroke:#7ea8d4,stroke-width:2px,color:#c0d8f0
    classDef data fill:#332a1a,stroke:#d4b870,stroke-width:2px,color:#f0e0c0
    classDef attack fill:#331a1a,stroke:#d97777,stroke-width:2px,color:#f0c0c0
    classDef highlight fill:#332519,stroke:#e8a87c,stroke-width:2px,color:#f0d8c0
    classDef success fill:#1a331a,stroke:#a8c686,stroke-width:2px,color:#c8e8b0

    T1["Phase 1\nPrice Manipulation\n(swap large amount)"]:::attack
    B1["|block| Boundary\nTimestamp advances"]:::highlight
    T2["Phase 2\nExploit Stale Price\n(borrow at wrong price)"]:::attack
    B2["|block| Boundary"]:::highlight
    T3["Phase 3\nExtract Profit\n(liquidate position)"]:::success

    T1 --> B1 --> T2 --> B2 --> T3

9. Related Work

The application of program synthesis to security has precedent in several domains. AEG (Automatic Exploit Generation) [Avgerinos et al., 2011] used symbolic execution to generate control-flow hijacking exploits for x86 binaries, framing the problem as a constraint satisfaction task over memory layouts. Our work differs in the state model (blockchain world state vs. process memory) and the execution semantics (deterministic state machine vs. non-deterministic concurrent execution).

In the blockchain domain, Mythril [Mueller, 2018] and Manticore [Mossberg et al., 2019] use symbolic execution to find constraint-satisfying inputs for vulnerability conditions but do not synthesize multi-step exploits or handle flash loan composition. ItyFuzz [Shou et al., 2023] applies coverage-guided fuzzing to smart contracts, which can be seen as a stochastic search over the exploit space without the grammar-based structuring we propose. ETHBMC [Frank et al., 2020] applies bounded model checking to EVM bytecode, providing exhaustive verification within bounds but without explicit exploit construction.

The SyGuS framework was introduced by Alur et al. [2013] and has been applied to program repair [Mechtaev et al., 2016], superoptimization [Phothilimthana et al., 2016], and invariant inference [Padhi et al., 2016]. The CEGIS paradigm originates with Solar-Lezama et al. [2006] in the Sketch synthesizer. Our adaptation replaces the SMT-based verifier with a concrete execution oracle, trading completeness for practical scalability—a tradeoff appropriate for the exploit domain where a single concrete witness suffices.

Template-based synthesis has been explored extensively in the program repair literature [Long and Rinard, 2015] where fix templates constrain the search for patches. Our finding-guided pruning is analogous: static analysis findings serve the same role as fault localization in constraining where and how a synthesized program should operate.

The formal treatment of smart contract security through programming language theory is an active area. Grossman et al. [2018] and Albert et al. [2020] have applied concurrency theory and resource analysis to smart contracts. Our contribution is specifically the synthesis framing—treating exploit generation not as analysis or verification but as constructive program generation within a formal framework.

10. References

1. Alur, R., Bodik, R., Juniwal, G., Martin, M. M. K., Raghothaman, M., Seshia, S. A., Singh, R., Solar-Lezama, A., Torlak, E., and Udupa, A. “Syntax-Guided Synthesis.” Proceedings of Formal Methods in Computer-Aided Design (FMCAD), 2013. https://doi.org/10.1109/FMCAD.2013.6679385

2. Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., and Saraswat, V. “Combinatorial Sketching for Finite Programs.” Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2006. https://doi.org/10.1145/1168857.1168907

3. Avgerinos, T., Cha, S. K., Hao, B. L. T., and Brumley, D. “AEG: Automatic Exploit Generation.” Proceedings of the Network and Distributed System Security Symposium (NDSS), 2011.

4. Mueller, B. “Smashing Ethereum Smart Contracts for Fun and Real Profit.” 9th Annual HITB Security Conference, 2018.

5. Mossberg, M., Manzano, F., Hennenfent, E., Groce, A., Grieco, G., Feist, J., Brunson, T., and Dinaburg, A. “Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts.” Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2019. https://doi.org/10.1109/ASE.2019.00133

6. Shou, C., Tan, S., and Sen, K. “ItyFuzz: Snapshot-Based Fuzzer for Smart Contract.” Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2023. https://doi.org/10.1145/3597926.3598059

7. Frank, J., Aschermann, C., and Holz, T. “ETHBMC: A Bounded Model Checker for Smart Contracts.” Proceedings of the 29th USENIX Security Symposium, 2020.

8. Mechtaev, S., Yi, J., and Roychoudhury, A. “Angelix: Scalable Multiline Program Patch Synthesis via Symbolic Analysis.” Proceedings of the 38th International Conference on Software Engineering (ICSE), 2016. https://doi.org/10.1145/2884781.2884807

9. Long, F. and Rinard, M. “Staged Program Repair with Condition Synthesis.” Proceedings of the 10th Joint Meeting on Foundations of Software Engineering (FSE), 2015. https://doi.org/10.1145/2786805.2786811

10. Padhi, S., Sharma, R., and Millstein, T. “Data-Driven Precondition Inference with Learned Features.” Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2016. https://doi.org/10.1145/2908080.2908099

11. Grossman, S., Abraham, I., Golan-Gueta, G., Michalevsky, Y., Rinetzky, N., Sagiv, M., and Zohar, Y. “Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts.” Proceedings of the ACM on Programming Languages (POPL), 2018. https://doi.org/10.1145/3158136

12. Albert, E., Correas, J., Gordillo, P., Roman-Diez, G., and Rubio, A. “SAFEVM: A Safety Verifier for Ethereum Smart Contracts.” Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2020. https://doi.org/10.1145/3395363.3404366

13. Phothilimthana, P. M., Thakur, A., Bodik, R., and Dhurjati, D. “Scaling Up Superoptimization.” Proceedings of the 21st International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2016. https://doi.org/10.1145/2872362.2872387

14. Bernstein, P. A., Hadzilacos, V., and Goodman, N. Concurrency Control and Recovery in Database Systems. Addison-Wesley, 1987. ISBN 0-201-10715-5.