AutoStub: Genetic Programming-Based Stub Creation for Symbolic Execution

Felix M\"achtle; Jan-Niclas Serr; Jonas Sander; Nils Loose; Thomas Eisenbarth

REVIEW 4 major objections 6 minor 1 cited by

AutoStub: Genetic Programming-Based Stub Creation for Symbolic Execution

T0 review · 4 major / 6 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read AutoStub uses genetic programming to turn random input-output samples into symbolic stubs, letting symbolic execution pass external calls.

desk verdict A reasonable GP-based stub generator with credible RQ1 numbers, but the RQ2 benchmark makes the symbolic-execution success nearly tautological. read the letter →

arxiv 2509.08524 v1 pith:OID67OFQ submitted 2025-09-10 cs.SE cs.AIcs.CR

Felix Mächtle , Nils Loose , Jan-Niclas Serr , Jonas Sander , Thomas Eisenbarth This is my paper · ORCID

classification cs.SEcs.AIcs.CR

keywords symbolicexecutiongeneticprogrammingstubgenerationexternalfunctionsgrammar-guidedblack-boxapproximationSMT-LIBoperatorsJavalibrary

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Symbolic execution explores program paths by treating inputs as formulas, but it stalls when the program calls an external function whose behavior cannot be expressed symbolically. AutoStub removes that stall automatically: it runs the external function on randomly generated inputs, uses grammar-guided genetic programming to evolve a symbolic expression that matches the observed input-output pairs, and inserts that expression as a stub. The authors show that 55% of the 273 Java standard-library functions they tested are approximated with over 90% correctness on fresh random inputs, and that the resulting stubs let a Java symbolic executor solve most benchmark paths in well under a second. If this holds, symbolic execution could explore paths through third-party and native calls without manual modeling, and the evolved expressions can expose edge cases that human-written stubs might miss.

What carries the argument

The central mechanism is grammar-guided genetic programming over a type-consistent grammar built from 40 SMT-LIB operators. Candidate expression trees evolve through tournament selection, one-point crossover, and subtree mutation, with fitness tailored to the output type: normalized root mean squared error for numeric outputs, classification accuracy for booleans, and Levenshtein distance for strings. Input generation uses stratified sampling across bit-lengths and floating-point exponents to cover many magnitudes, plus special values such as NaN, Infinity, and 0, 1, or −1 with 5% probability. The evolved expression replaces the external call during symbolic execution, letting the executor c

What would settle it

Run AutoStub on the 273 benchmark functions, then evaluate the generated stubs on inputs sampled from concrete branch constraints collected while symbolically executing real client programs that call these functions. If agreement on those path-derived inputs falls materially below the 90% correctness reported for random inputs, the representativeness assumption is refuted.

Watch

Extended reading notes

Core claim

AutoStub claims that black-box external functions can be approximated well enough for symbolic execution by evolving closed-form expressions from random input-output data alone. On 273 methods drawn from Java's primitive, string, Math, and StrictMath classes, an evolved expression predicts the correct output on more than 90% of fresh random inputs for 55% of the functions. Inserting these expressions as symbolic stubs into a Java symbolic execution engine solves most benchmark tests, with an average solving time of 0.04 seconds. A striking result is the evolved expression for Double.isNaN: the formula !(−1 < |x|) correctly captures Java's rule that any comparison involving NaN is false, show

Load-bearing premise

The random stratified inputs used to train and evaluate stubs represent the inputs a real program will actually pass to the external function; if real program paths concentrate on different values, the headline accuracy will not transfer.

Editorial extensions

If this is right

A symbolic executor can keep exploring paths through an external Java primitive or string call instead of stopping, with no hand-written stub.
The evolved stubs are compact expressions that SMT solvers handle quickly, with typical benchmark solve times below one tenth of a second.
Without a prior model of Java's float semantics, AutoStub can discover behavior such as NaN comparisons being false, which is directly useful for edge-case testing.
Stubs that encode language-specific semantics can be correct in Java yet hard for an SMT solver to interpret, so solver-compatible encodings are needed for full coverage.
The benchmark of 10 tests per function, each requiring two distinct outputs, gives a conservative way to measure whether a stub is truly learning behavior rather than returning a constant.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Beyond the paper: the random stratified sampling could be replaced or augmented with inputs drawn from constraints collected during real symbolic paths, making stubs accurate exactly where they are used.
Beyond the paper: AutoStub's evolved expressions are human-readable formulas, so they could double as documentation or as oracles for differential testing against the real function.
Beyond the paper: the same GP pipeline could be extended to stateful objects by approximating sequences of calls to a final primitive output, which the authors note as future work.
Beyond the paper: the accuracy reported on random inputs is an upper bound for realistic use; measuring stub agreement on path-derived inputs would show how much of the 90% transfers to actual programs.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Short version: this is a genuine first use of grammar-guided GP for symbolic stubs, and the RQ1 numbers are credible for the narrow scope. But the RQ2 evaluation doesn't measure what it claims, and the paper's path-exploration headline is not supported.

What's new: AutoStub uses G3P to fit expressions to input-output samples from external Java functions, then plugs those expressions into the SWAT symbolic executor. That's a legitimate extension of symbolic regression to stub generation; I don't know of prior GP-based stub work. The paper ships code and data, and the limitations section is honest: stateless functions only, regular-complexity expressions, and the Java/Z3 floating-point semantics gap.

The good: RQ1 uses 10^6 fresh samples per function, so the 55%-over-90% figure is not fitting the evaluation points. For simple stateless functions over primitives and strings, that's a reasonable result, and the Double.isNaN expression (!(−1 < |x|)) is a nice example of GP discovering Java's NaN comparison semantics.

The soft spot is RQ2, and it's the load-bearing one. The symbolic-execution benchmark is built by drawing random inputs from the same stratified distribution used to train the stubs, and then only expressions that already scored >90% on that distribution are admitted into the symbolic-execution test. So the solve rates in Figure 2 are almost a restatement of the accuracy filter. The tests check two random points with distinct outputs; a stub that matches the training distribution will pass most of those by construction. That does not demonstrate that stubs work on inputs that actually arise along realistic path conditions—where values cluster near boundaries, NaN/Infinity, empty strings, or values satisfying prior predicates. So the claim about exploring previously intractable paths is not established. It's at most 'stubs fit the training distribution on hand-made test programs.'

Minor issues: no GP hyperparameters or run-to-run variance; no comparison to existing automated stub methods; exact-match comparison for floating point is not discussed. The floating-point mismatch with Z3 is acknowledged, but it weakens the RQ2 results precisely for the edge cases the paper highlights.

Who this is for: symbolic execution researchers and tool builders. The dataset and the RQ1 methodology are useful. I'd take it seriously as a workshop or short-paper contribution, but the evaluation needs to be redone with realistic path constraints, or at least with benchmark programs whose input distributions come from actual program paths. I'd send it to peer review with a request for major revision.

Referee Report

4 major / 6 minor

Summary. The paper proposes AutoStub, a grammar-guided genetic programming (G3P) system that automatically generates symbolic stubs for external Java functions during symbolic execution. AutoStub samples random stratified inputs, executes the external function to collect input-output pairs, and evolves expressions over 40 SMT-LIB operators. The generated expressions are then used as stubs in the SWAT symbolic executor. The evaluation targets 273 Java standard-library methods and reports two main results: (RQ1) 55% of generated expressions achieve over 90% correctness on freshly sampled random inputs, and (RQ2) high-accuracy expressions, when integrated into SWAT, solve most of a purpose-built benchmark of 2,730 small test programs. The paper also highlights an inferred approximation for Double.isNaN and discusses limitations for stateful functions and non-regular-complexity behaviors.

Significance. If the evaluation were fully convincing, AutoStub would be a useful step toward reducing manual stub writing for symbolic execution. The paper has real strengths: RQ1 uses a fresh evaluation set rather than reusing training data, a random fitness baseline is reported, and the repository and benchmark are promised as public artifacts. The central accuracy claim is credible for simple primitive/string functions on random inputs. However, the RQ2 benchmark is constructed from the same random input distribution used to train the stubs, so the symbolic-execution success rates largely reflect fitting that distribution rather than usefulness under realistic path constraints. The missing GP hyperparameters and the brittle floating-point matching further weaken the claims. I view the contribution as a solid empirical starting point, but the paper currently overstates what is established.

major comments (4)

[§III-B, §IV-B] The RQ2 evaluation is nearly tautological. The symbolic-execution benchmark is built by drawing two random inputs from the same stratified distribution used in §III-A for training and RQ1 evaluation, computing distinct outputs (o1, o2), and testing whether the stub satisfies y1=o1 ∧ y2=o2. Section IV-B then selects only expressions that already score >90% on that exact distribution. A stub with >90% accuracy on the distribution will pass most two-point random tests by construction, so Figure 2's solve rates do not measure whether the stubs are useful on inputs that actually arise along realistic symbolic-execution paths, where path conditions concentrate values near boundaries, NaN/Infinity, empty strings, or previously constrained subdomains. The conclusion that AutoStub "enables exploration of program paths that were previously intractable" is therefore not established by the data. I r
[§IV-A] The accuracy metric for floating-point functions is not specified beyond "the output matched the expected value." If this is exact Java double/float equality, the metric is extremely brittle and can understate the quality of a numerically correct approximation, while accidentally rewarding expressions that merely round to the same value. The paper should state whether exact equality is used and, if so, also report a tolerance-based or ULP-based error metric for floating-point outputs. This is load-bearing because RQ1's headline 55% figure depends entirely on this definition of correctness.
[§II, §III-A, §IV] The paper omits the GP hyperparameters needed to reproduce the experiments: population size, number of generations, mutation and crossover rates, tournament size, the proportion of special values, and the grammar used for type consistency. It is also unclear whether each function was evolved once or multiple times; GP is stochastic, and Figure 1 appears to aggregate only one run per method. Without this information and some measure of run-to-run variance, the RQ1 accuracy distribution cannot be assessed as a stable property. Please add a configuration table and, ideally, report means and standard deviations over several independent runs.
[§IV-B, §V] Even if the random-input benchmark were accepted, the paper's end-to-end claim is further limited by the solver-semantics gap acknowledged in §IV-B: expressions that capture Java-specific behavior, such as NaN comparisons, cannot always be interpreted correctly by Z3. Combined with the §V restrictions to stateless functions and regular-complexity expressions, the actual class of functions for which AutoStub can replace manual stubs in practice is much narrower than the abstract suggests. This is not a fatal flaw, but the conclusion should be reframed to state that AutoStub works for simple stateless primitive/string functions whose learned expressions stay within SMT-LIB semantics.

minor comments (6)

[§IV-A] The text says "106 new input-output pairs"; this should be typeset as 10^6 (1000000) if that is the intended count, otherwise the sentence is ambiguous.
[§IV-A] The random baseline is described only as "fitness values were randomly assigned." Please state concretely what was randomized and how it was compared with the GP runs, since the 15% versus 55% comparison is a key benchmark for RQ1.
[§IV-B] The paragraph beginning "A small subset of nine..." is unclear: are these nine expressions among the high-accuracy set selected for Figure 2? If so, what are their accuracies and why do they still cause failures? Also, the example "multiplication of two large integers (x × y = 391,768,351,037,400,960)" lacks the specific input values x and y.
[§III-A] The special-value sampling probability is stated as 5% but no table or list of which special values are included for each type is given. This is important because hits on edge cases like NaN or Integer.MAX_VALUE may dominate the reported accuracy and solving behavior.
[§II] The grammar used for G3P is not shown or described beyond the operator count. Since the grammar largely determines the search space, please include it in the paper or at least in the repository with a clear pointer.
[Throughout] Minor text issues: "SMT-Lib" should be "SMT-LIB"; "A UTO STUB" contains stray spacing; the reference list entries for [1]–[11] lack complete publication venues and years in several cases; and Figure 2's legend (“Correct”, “90% correct”) should be explained in the caption.

Circularity Check

1 steps flagged · score 6.0 of 10

RQ2's symbolic-execution benchmark is drawn from the same random-input distribution used to train and select stubs, so the reported solve rates largely re-test RQ1 accuracy rather than demonstrating generalization to realistic path constraints.

fitted input called prediction [Section III-B (Symbolic Execution Dataset) and Section IV-B (Symbolic Execution with Generated Expressions)]
"For every external function f, we generated two random input values and observed the corresponding output values ... we created a benchmark dataset consisting of Java classes that check whether the external function f returns the desired output values (o1, o2) for given inputs. ... We selected all expressions from RQ1 that achieved an accuracy higher than 90% and integrated them into SW AT [5]."

The RQ2 benchmark is built from random input-output pairs sampled with the same stratified input-generation strategy (Section III-A) used to train and evaluate the GP expressions. Only expressions already showing >90% accuracy on that exact input distribution are admitted to RQ2. Each benchmark test simply checks two random inputs against the observed outputs, so a stub with >90% in-distribution accuracy will pass most of these tests by construction. The solve rates in Figure 2 therefore largely re-express the RQ1 accuracy filter; they do not measure behavior on inputs that arise from realistic path conditions during symbolic execution. Consequently, the claim that AutoStub 'allow[s] the symbolic executor to continue the analysis ... enabling the exploration of program paths that were prev

full rationale

The core GP-based approximation pipeline is not itself circular: RQ1 evaluates on 10^6 newly generated input-output pairs from the same distribution, which is a legitimate held-out accuracy measurement, and the random baseline provides a meaningful comparison. The self-citation to SWAT [5] is not load-bearing for the derivation; it is just the execution engine used in the experiment. The main circularity is concentrated in RQ2. The benchmark programs are constructed by sampling two random inputs from the same stratified distribution used for training and RQ1 evaluation, and only expressions that already scored >90% on that distribution are selected. Thus the symbolic-execution success rate is a near-tautological consequence of the accuracy filter, not evidence that stubs generalize to inputs concentrated by path constraints (boundaries, NaN/Infinity, empty strings, values satisfying prior predicates). The paper's Section V limitations further narrow the scope but do not repair this distribution gap. Because the central 'path exploration' claim is supported by an evaluation that reduces, with high probability, to the training/evaluation distribution fit, a score of 6 is appropriate: partial circularity in the central claim, though the GP expression search itself retains independent content.

Assumptions & free parameters 5 free parameters · 4 assumptions · 0 invented entities

No fundamentally new entities are introduced. The method relies on GP hyperparameters (underspecified), random input sampling choices, and assumptions about the representativeness of the input distribution and the mapping of Java float semantics to Z3. These assumptions are either stated limitations or unverified claims.

free parameters (5)

GP population size = not reported
The number of candidate expressions per generation is not stated; the success rate of stub generation likely depends on it.
GP number of generations = not reported
Not stated; more generations can improve fit but increase runtime.
Mutation and crossover rates = not reported
Genetic operator probabilities are not specified, so the search dynamics are underspecified.
Tournament selection size = not reported
Tournament selection is mentioned but no tournament size is given.
Special value proportion = 0.05
The probability of injecting special values (NaN, Infinity, 0, 1, -1, max/min) into training data is a hand-chosen hyperparameter affecting which edge cases the GP sees.

assumptions (4)

domain assumption External functions under analysis are stateless and side-effect-free
Stated in Section V as a limitation; all 273 selected methods must not have side effects on the caller. This restricts the scope of the central claim.
domain assumption The random stratified sampling distribution (Section III-A) is representative of inputs encountered on real symbolic execution paths
No evidence is provided that real program path constraints concentrate inputs similarly; the accuracy and solve-rate results depend on this.
domain assumption Java floating-point semantics (NaN, Infinity) can be expressed in SMT-LIB for Z3
The paper itself shows this fails for some expressions: Z3 handles NaN differently (Section IV-B), causing benchmark failures.
ad hoc to paper The 40-operator SMT-LIB grammar is expressive enough to capture behaviors of the target functions
The operator set is selected 'to cover the majority of Java scenarios' (Section III); functions requiring constructs outside this grammar cannot be approximated.

how reviews work

0 comments

Cite this review

Pith. "Pith review of AutoStub: Genetic Programming-Based Stub Creation for Symbolic Execution." pith.science (2026). https://pith.science/paper/OID67OFQ

@misc{pith2026250908524,
  author       = {Pith},
  title        = {Pith review of: AutoStub: Genetic Programming-Based Stub Creation for Symbolic Execution},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/OID67OFQ}},
  note         = {Machine review of arXiv:2509.08524}
}

read the original abstract

Symbolic execution is a powerful technique for software testing, but suffers from limitations when encountering external functions, such as native methods or third-party libraries. Existing solutions often require additional context, expensive SMT solvers, or manual intervention to approximate these functions through symbolic stubs. In this work, we propose a novel approach to automatically generate symbolic stubs for external functions during symbolic execution that leverages Genetic Programming. When the symbolic executor encounters an external function, AutoStub generates training data by executing the function on randomly generated inputs and collecting the outputs. Genetic Programming then derives expressions that approximate the behavior of the function, serving as symbolic stubs. These automatically generated stubs allow the symbolic executor to continue the analysis without manual intervention, enabling the exploration of program paths that were previously intractable. We demonstrate that AutoStub can automatically approximate external functions with over 90% accuracy for 55% of the functions evaluated, and can infer language-specific behaviors that reveal edge cases crucial for software testing.

Figures

Figures reproduced from arXiv: 2509.08524 by the authors.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Prompt Pirates Need a Map: Stealing Seeds helps Stealing Prompts
cs.CR 2025-09 conditional novelty 6.0 of 10

Diffusion image tools inherit a 32-bit seed weakness from PyTorch, letting an attacker recover the seed in about 140 minutes and then use it, via a genetic algorithm, to steal the prompt behind a public image.

Reference graph

Works this paper leans on

11 extracted references · cited by 1 Pith paper

[1]

A survey of symbolic execution techniques

Roberto Baldoni, Emilio Coppa, Daniele Cono D’Elia, Camil Deme- trescu, and Irene Finocchi. A survey of symbolic execution techniques. 2018

2018
[2]

The smt-lib standard: Version 2.0

Clark Barrett, Aaron Stump, Cesare Tinelli, et al. The smt-lib standard: Version 2.0. 2010

2010
[3]

Foster, and Armando Solar-Lezama

Jinseong Jeon, Xiaokang Qiu, Jonathan Fetter-Degges, Jeffrey S. Foster, and Armando Solar-Lezama. Synthesizing framework models for symbolic execution. 2016

2016
[4]

James C. King. Symbolic execution and program testing. 1976

1976
[5]

SW AT: modular dynamic symbolic execution for java applications using dynamic instrumentation (competition contribution)

Nils Loose, Felix M ¨achtle, Florian Sieck, and Thomas Eisenbarth. SW AT: modular dynamic symbolic execution for java applications using dynamic instrumentation (competition contribution). 2024

2024
[6]

Symbolic execution with existential second-order con- straints

Sergey Mechtaev, Alberto Griggio, Alessandro Cimatti, and Abhik Roychoudhury. Symbolic execution with existential second-order con- straints. 2018

2018
[7]

Anh T. V . Nguyen and Mizuhito Ogawa. Automatic stub generation for dynamic symbolic execution of ARM binary. 2022

2022
[8]

java.lang (Java SE 17 & JDK 17)

Oracle. java.lang (Java SE 17 & JDK 17). https://docs.oracle.com/en/ java/javase/17/docs/api/java.base/java/lang/package-summary.html. Ac- cessed 10/2024

2024

Show all 11 references

[9]

Sumner, Feng Qin, Mai Zheng, Xiangyu Zhang, and Abhik Roychoudhury

Dawei Qi, William N. Sumner, Feng Qin, Mai Zheng, Xiangyu Zhang, and Abhik Roychoudhury. Modeling software execution environment. 2012

2012
[10]

Grammatically-based genetic programming

Peter A Whigham et al. Grammatically-based genetic programming. 1995

1995
[11]

Automatic model generation from documentation for java API functions

Juan Zhai, Jianjun Huang, Shiqing Ma, Xiangyu Zhang, Lin Tan, Jianhua Zhao, and Feng Qin. Automatic model generation from documentation for java API functions. 2016

2016

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.

[1] [1]

A survey of symbolic execution techniques

Roberto Baldoni, Emilio Coppa, Daniele Cono D’Elia, Camil Deme- trescu, and Irene Finocchi. A survey of symbolic execution techniques. 2018

2018

[2] [2]

The smt-lib standard: Version 2.0

Clark Barrett, Aaron Stump, Cesare Tinelli, et al. The smt-lib standard: Version 2.0. 2010

2010

[3] [3]

Foster, and Armando Solar-Lezama

Jinseong Jeon, Xiaokang Qiu, Jonathan Fetter-Degges, Jeffrey S. Foster, and Armando Solar-Lezama. Synthesizing framework models for symbolic execution. 2016

2016

[4] [4]

James C. King. Symbolic execution and program testing. 1976

1976

[5] [5]

SW AT: modular dynamic symbolic execution for java applications using dynamic instrumentation (competition contribution)

Nils Loose, Felix M ¨achtle, Florian Sieck, and Thomas Eisenbarth. SW AT: modular dynamic symbolic execution for java applications using dynamic instrumentation (competition contribution). 2024

2024

[6] [6]

Symbolic execution with existential second-order con- straints

Sergey Mechtaev, Alberto Griggio, Alessandro Cimatti, and Abhik Roychoudhury. Symbolic execution with existential second-order con- straints. 2018

2018

[7] [7]

Anh T. V . Nguyen and Mizuhito Ogawa. Automatic stub generation for dynamic symbolic execution of ARM binary. 2022

2022

[8] [8]

java.lang (Java SE 17 & JDK 17)

Oracle. java.lang (Java SE 17 & JDK 17). https://docs.oracle.com/en/ java/javase/17/docs/api/java.base/java/lang/package-summary.html. Ac- cessed 10/2024

2024