Pith. sign in

REVIEW 3 major objections 5 minor 38 references

Program Synthesis from Partial Traces

T0 review · 3 major / 5 minor · reviewed 2026-08-16 · deepseek-v4-flash

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

Pith's one-line read Syren synthesizes complete API scripts from partial call logs, hidden steps included.

desk verdict Genuinely new synthesis problem with a sensible rewrite-plus-PBE decomposition, but the correctness guarantee is narrower than the abstract suggests and the appendix has data errors that should be fixed. read the letter →

arxiv 2504.14480 v3 pith:3A5A3I7M submitted 2025-04-20 cs.PL

Margarida Ferreira , Victor Nicolet , Joey Dodds , Daniel Kroening This is my paper · ORCID
classification cs.PL
keywords programsynthesispartialtracessyntax-guidedrewritingAPIcompositionprogrammingbyexampletracesubsumptioncloudautomation
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

The paper introduces Syren, a synthesis technique that takes only partial traces—recorded sequences of side-effecting API calls, with no record of the pure computations between them—and produces a script that composes those calls with the missing pure functions and control flow. The central claim is that this problem is solvable without negative examples or extra user input, and Syren is presented as the first method to do so. The algorithm generalizes over the positive traces, using a user-defined cost metric to pick among generalizations, and the output is correct by construction in the paper's sense: it provably reproduces every input trace. A sympathetic reader should care because the same machinery applies wherever traces are already being recorded—API automation logs, system-call logs, document-editing logs—so synthesis costs no extra specification effort.

What carries the argument

The load-bearing mechanism is a pair of rewrite systems over a small domain-specific language: refinement rules, which factor identical visible calls out of conditionals and eliminate unused parameters while preserving trace subsumption, and synthesis rules, which replace an expression or branch condition with a call to a to-be-synthesized pure function. Correctness of the latter is tracked by a trace valuation, an augmented state that records, for every input trace, the concrete value each program variable must take. From that valuation the synthesizer extracts input-output pairs for the hidden function, such as a condition that reads the response of a status call and decides whether to retry, and discharges them to a programming-by-example solver; a rewrite is admitted only when such an implementation exists. The whole search is steered by a user-supplied cost function, so the final program minimizes that cost among all programs that still reproduce the traces.

What would settle it

Take one API resource whose state changes with time, call the same sequence of visible functions twice with a long pause between the runs, and record the two traces; if the only difference is the response to a later status call, the ordering-only semantics predicts that no synthesized program can reproduce both traces, so either Syren fails or it must abandon the exact-reproduction guarantee.

Watch

Extended reading notes

Core claim

On its own terms, the discovery is that a program can be synthesized from a partial trace by starting from a trivially correct program that replays each trace on its own branch, then repeatedly rewriting that program to hoist shared calls, replace constants with parameters, and replace branch conditions with calls to newly synthesized pure functions. Each rewrite is proved to preserve trace subsumption, meaning the new program can still generate every input trace; the hidden functions are obtained by converting the current trace valuation into input-output examples and solving them with an off-the-shelf syntax-guided synthesizer. This is the first approach, the authors argue, to infer both control flow and non-trivial hidden pure function calls from records of only the side-effecting functions. The paper further claims that the approach scales to 54 real-world benchmarks drawn from cloud automation, filesystem, and document-edition scripts, with 39 of them synthesized optimally in under five minutes.

Load-bearing premise

The whole guarantee rests on the assumption that a visible function's response is determined by the ordered sequence of earlier visible calls, not by how much wall-clock time has passed; real APIs whose replies change over time are outside the model.

Editorial extensions

If this is right

  • Programs synthesized this way can include conditionals, retry loops, and hidden pure functions that never appear in the traces, yet each synthesized program is guaranteed to reproduce every input trace.
  • A user needs to supply only positive traces; no negative examples are required, because the cost function, not counterexamples, prevents over-generalization.
  • Swapping the cost function changes the notion of best program: the paper demonstrates syntactic-complexity and trace-reuse metrics, and both are usable within the same rewrite framework.
  • The correctness guarantee is conditional: it holds when visible-function responses are a function of the ordered sequence of prior calls, as the paper states in its semantics section.
  • The main bottleneck is the underlying programming-by-example solver, so any improvement in JSONPath, string, or arithmetic synthesis would directly extend Syren's reach.

Reading between the lines

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

  • If the ordering-only assumption is relaxed, the same rewrite machinery could target timeout-driven retries and rate-limit responses, which are visible-call sequences whose outputs depend on elapsed time; the paper's own limitation note identifies exactly this boundary.
  • A practical extension would be to let a large language model propose hidden-function implementations and then run Syren's trace-subsumption check as a verifier, converting silent failures into detectable ones.
  • Because the cost function is user-defined, the framework could optimize for operational properties beyond readability, such as fewest distinct API endpoints or least-privilege permission sets, which would matter for security-sensitive automation.
  • The benchmark suite is built by simulating traces that exercise all program paths; a natural next experiment is to measure how few traces are needed per control-flow structure, since the paper reports 2 to 10 traces per benchmark.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper introduces Syren, a synthesis technique that takes a set of partial execution traces -- records of only the visible side-effecting calls -- and produces a program that composes those visible calls with hidden pure functions and control-flow constructs such as conditionals and retry loops. The technical approach starts from a trivially correct program that branches over the input traces and repeatedly applies two kinds of rewrite rules: refinement rules that preserve trace subsumption, and synthesis rules that introduce hidden functions whose implementations are obtained from an off-the-shelf syntax-guided synthesizer. Correctness is formalized as trace subsumption: a program is correct if it can reproduce the input traces for some input state. The paper reports an implementation and evaluates it on 54 benchmarks from custom cloud-automation tasks, AWS runbooks, Blink automations, and ApiPhany-derived examples, finding that the main algorithm synthesizes the target-quality program for 39 of 54 benchmarks under the syntactic cost function. The claimed contributions are the first partial-trace synthesis formulation, the combining of optimizing rewrites with SyGuS, and the benchmark evaluation.

Significance. If the formal correctness claim is stated precisely, the paper describes a practically motivated and technically interesting synthesis problem that has not been addressed as a whole before. The combination of optimizing program rewrites with programming-by-example synthesis of hidden functions is a sensible decomposition of a hard search problem, and the evaluation on 54 benchmarks, with reproducible code and data, gives useful evidence about scalability. The paper also honestly documents several limitations, including unsupported date/string operations, inability to handle empty traces that terminate before any visible call, and timeouts on complex control flow. However, the headline 'correct by construction' guarantee is currently tied to an under-specified notion of global state, which affects the central formal claim rather than only the presentation.

major comments (3)
  1. [§3.3, Definition 3.2, and §4.1, Eq. (1)] The correctness predicate Ψ in Eq. (1) quantifies only over a local state σ, but Definition 3.2 and the Visible rule in Figure 5 define program evaluation relative to an initial global state G that is implicitly updated by each visible call. As written, P(σ)=τ is not a well-defined two-argument predicate, and the headline claim that the synthesized program 'will always be able to reproduce the input traces' is not entailed by Ψ. The motivating EC2 example in §2 illustrates the difficulty: the first two traces share the visible prefix StopInstances(force=false); DescribeInstanceStatus but observe 'stopping' in one trace and 'stopped' in the other, so no deterministic order-only transition from a single global state can produce both. The paper's own caveat in §3.3 -- that the approach is unsound when responses depend on time as opposed to ordering -- applies directly to this example. I recommend making the global state explicit in Definition 3.2 and Eq. (1), for instance by quantifying existentially over an initial global state per input trace, and then restating the correctness claim as per-trace replay under a matching initial state, or by substantially extending the semantics to model time dependence.
  2. [§5.1, trace-valuation correctness implication] The formal framework for rewrite correctness is stated as a single implication below the definition of the trace valuation transformation, but that implication is not a complete theorem: it does not specify the quantifier structure over global states, does not state whether the conclusion must hold for the same global state as the hypothesis, and no proof is provided that the transformation t always produces a trace valuation satisfying the invariant. Since this implication is what justifies 'correct by construction' for every synthesis rewrite, the paper needs a rigorous statement and proof, or at minimum a precise invariant that is shown to be preserved by each rewrite rule.
  3. [§7.2, Table 1] The evaluation defines success as syntactic equivalence, modulo variable renaming, to a target program that the authors themselves wrote, and the input traces are generated by simulating those same target programs. Consequently, the 39/54 'optimal' result measures agreement with the authors' hand-written targets under the authors' cost functions, rather than an independent measure of whether the synthesized program is the correct generalization of the observed behavior. This limitation should appear in the main text, not only implicitly in the benchmark description, and the manual inspection step used to decide when enough traces had been collected should be documented more transparently.
minor comments (5)
  1. [§3.2 and Figure 5] The trace definition in §3.2 records a visible call as (A(v), e), while the Visible rule in Figure 5 produces (A(G, v), e); the global-state parameter in the trace record should either be removed or explained.
  2. [Appendix D.1.18] The benchmark WaitForInputThenSendEmail uses the variable `_r` in the retry body but later refers to `payload`, and the SendEmail call passes `userId=isNonEmpty` rather than a value; if this is the actual benchmark code, it should be corrected or clarified.
  3. [Table 1] The row for Report Long Running Instances reports '#Hidden-f' as -1 and '#If' as '??'; these placeholders should be replaced with concrete values or an explicit explanation of why they are not available.
  4. [Appendix C] The LLM prompt explicitly instructs the model not to add loops when the traces do not show a need for them; this design choice can bias the comparison in favor of simpler programs and should be disclosed when interpreting the LLM results.
  5. [§6.1 and §7.4] The k-bounded search uses a fixed k=6, and the text notes that increasing k leads to an intractable search space; a short sensitivity statement about how the results depend on k would make the comparison more interpretable.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: correctness is explicitly defined as trace reproduction, and each rewrite is checked against that same specification via trace subsumption; hidden functions are synthesized from trace-derived input-output examples, which is standard PBE rather than a disguised prediction.

full rationale

The derivation chain is self-contained. The initial program P_in is built directly from T_in so that Ψ(P_in,T_in) holds by construction (§4.1, Fig. 8). Refinement rules are required to preserve trace subsumption, and Lemma 1 transfers correctness: if P'⊒P and Ψ(P,T_in), then Ψ(P',T_in). Synthesis rules are accepted only when a hidden-function implementation f makes P'(f)⊒P_in; §5.2 reduces this obligation to input-output constraints φ(JxK)=v extracted from the trace valuation, and a sound PBE solver (Rosette/CVC5) provides f. This is a conventional synthesis loop in which the specification (reproduce the input traces) is also the correctness criterion, so the final guarantee is by construction rather than an independent prediction. The paper is explicit about the limits of that guarantee: the §2 footnote admits that with only two traces the solver returns a trace-memorizing function, and §3.3 states the ordering-only global-state model 'will be unsound in situations where responses implicitly depend on time as opposed to ordering.' These are overfitting and soundness caveats, not circular reductions. Self-citations ([15], [21], [28]) support parallelization detail, related-work context, and artifact access; none is load-bearing for the main theorem. The benchmarks are partly self-created, which affects external validity but not the internal derivation. No step in the paper equates a fitted parameter with an independent prediction or imports a uniqueness result from the authors' prior work.

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

The central claim rests mostly on the DSL semantics and the rewrite rules, which are self-contained. The main imported assumptions are about the external API behavior (order-dependence) and the expressiveness of the hidden-function synthesizer; neither is independently evidenced beyond the paper's own benchmarks.

free parameters (4)
  • syntactic cost weights (chi_syn) = 10 per statement, 1 per parameter, 1 per br usage
    Hand-chosen in §7.3 to prioritize fewer statements and parameters; used in the main evaluation.
  • trace reuse cost definition (chi_T) = total API calls + statements - reuse count, plus br penalty
    Hand-designed in §7.3 as an alternative metric; demonstrates cost-function flexibility.
  • retry bound K = greater than the longest input trace
    Introduced in §3.3 to guarantee termination of retry-until loops; a free choice the user or implementer must set.
  • k-bounded search depth = 6
    Parameter for the k-search baseline described in §6.1 and fixed in §7.4; not part of the core algorithm.
assumptions (4)
  • domain assumption Visible-function responses are determined by the ordered sequence of calls via an implicit global state, not by wall-clock time.
    Invoked throughout §3.3 and §4; the paper explicitly flags this as a source of unsoundness when time matters.
  • domain assumption Hidden functions are pure and restricted to the provided JSONPath/basic-operation DSL.
    Syren outsources hidden-function synthesis to Rosette over the grammar in Fig. 6; the paper reports failures for date/time and complex string tasks.
  • ad hoc to paper The user-supplied cost function is a suitable proxy for the desired generalization.
    The synthesis objective is to minimize chi over correct programs (§4.2); the final program's usefulness, as opposed to its trace-correctness, depends on this.
  • domain assumption At least two finite traces are provided.
    Assumed in §4.1 and §3.2; the initial program branches on br with |T_in| branches.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Program Synthesis from Partial Traces." pith.science (2026). https://pith.science/paper/3A5A3I7M

@misc{pith2026250414480,
  author       = {Pith},
  title        = {Pith review of: Program Synthesis from Partial Traces},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3A5A3I7M}},
  note         = {Machine review of arXiv:2504.14480}
}
read the original abstract

We present the first technique to synthesize programs that compose side-effecting functions, pure functions, and control flow, from partial traces containing records of only the side-effecting functions. This technique can be applied to synthesize API composing scripts from logs of calls made to those APIs, or a script from traces of system calls made by a workload, for example. All of the provided traces are positive examples, meaning that they describe desired behavior. Our approach does not require negative examples. Instead, it generalizes over the examples and uses cost metrics to prevent over-generalization. Because the problem is too complex for traditional monolithic program synthesis techniques, we propose a new combination of optimizing rewrites and syntax-guided program synthesis. The resulting program is correct by construction, so its output will always be able to reproduce the input traces. We evaluate the quality of the programs synthesized when considering various optimization metrics and the synthesizer's efficiency on real-world benchmarks. The results show that our approach can generate useful real-world programs.

Figures

Figures reproduced from arXiv: 2504.14480 by the authors.

Figure 1
Figure 1. Overview of our synthesis approach. might repeatedly follow a sequence of steps to create a data store and then attach an access policy to that data store. For convenience, they create a policy name by appending the string "policy" to an ID generated by the creation of the data store. The log of these actions kept on the cloud will contain the creation of the data store, the policy, and the connection between the tw… view at source ↗
Figure 2
Figure 2. Performing and monitoring actions on the AWS console [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Example of a program that stops an EC2 instance. [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figures from the paper (6 more)
Figure 4
Figure 4. Figure 4: Core scripting language. Expressions E can be visible or hidden function calls. A visible function call A(𝑥) is a call to some externally defined function A with arguments 𝑥, and a hidden call 𝑓 (𝑥) is a call to a pure function 𝑓 whose implementation F is defined in th…
Figure 5
Figure 5. Figure 5: Big-step semantics represents external resources accessed by the visible functions in the trace. The notion of global state is necessary because visible functions are not pure functions of their inputs; depending on the resources they access, two calls to the same func…
Figure 6
Figure 6. Figure 6: Hidden functions synthesis DSL. The correctness of the result of applying a synthesis rewrite rule 𝑃 ⇝ 𝑃 ′ (𝑓 ) depends on satisfying a set of constraints imposed on 𝑓 by the condition ∃𝑓 .𝑃′ (𝑓 ) ⊒ 𝑃𝑖𝑛. As we ex￾plained in the previous section, all rewrite rules updat…
Figure 8
Figure 8. Figure 8: The initial program 𝑃𝑖𝑛 takes a single integer parameter br, and has |𝑇𝑖𝑛 | branches, where each branch 𝑖 simply replays the visible function calls in trace 𝜏𝑖 ∈ 𝑇𝑖𝑛. 𝐴 𝑞 𝑖 is the 𝑖-th function call in trace #𝑞, and 𝑥 𝑞 𝑖 its corresponding input. UNSAT SAT Yes Yes No N…
Figure 7
Figure 7. Figure 7: Cost-directed alternating rewrite rule application. [PITH_FULL_IMAGE:figures/full_fig_p015_7.png]
Figure 9
Figure 9. Figure 9: Comparison of synthesis times and quality of synthesized programs using different search algorithms and cost functions. The background color in the heat map in 9b reflects the same data as the labels. In 9c, we show Syren’s ability to scale to complex benchmarks. The d…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

38 extracted references · 12 canonical work pages

  1. [1]

    Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. InFMCAD. IEEE, Portland, OR, USA, 1–8. https://doi.org/10.1109/FMCAD.2013.6679385

    arXiv 2013

  2. [2]

    Anthropic. 2024. Introducing Claude 3.5 Sonnnet. https://www.anthropic.com/news/claude-3-5-sonnet

    work page 2024

  3. [3]

    AWS. 2023. AWS Automation Runbooks Reference. https://docs.aws.amazon.com/systems-manager-automation- runbooks/latest/userguide/automation-runbook-reference.html. Proc. ACM Program. Lang., Vol. 9, No. PLDI, Article . Publication date: June 2025. Program Synthesis from Partial Traces 23

    work page 2023

  4. [4]

    AWS. 2023. What is AWS? https://aws.amazon.com/what-is-aws/

    work page 2023

  5. [5]

    Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. InTACAS. Springer, Munich, Germany, 415–442. ht...

    doi:10.1007/978-3-030-99524-9_24 2022

  6. [6]

    Chasins, Rastislav Bodík, and Sumit Gulwani

    Shaon Barman, Sarah E. Chasins, Rastislav Bodík, and Sumit Gulwani. 2016. Ringer: web automation by demonstration. InOOPSLA. ACM, Amsterdam, The Netherlands, 748–764. https://doi.org/10.1145/2983990.2984020

    arXiv 2016

  7. [7]

    Blink. 2023. Blink | The Security Automation Copilot. https://www.blinkops.com/

    work page 2023

  8. [8]

    Ricardo Brancas, Miguel Terra-Neves, Miguel Ventura, Vasco Manquinho, and Ruben Martins. 2024. Towards Reliable SQL Synthesis: Fuzzing-Based Evaluation and Disambiguation. InFASE. Springer, Luxembourg City, Luxembourg, 232–254. https://doi.org/10.1007/978-3-031-57259-3_11

    work page doi:10.1007/978-3-031-57259-3_11 2024

Show all 38 references
  1. [9]

    Tim Bray. 2017. The JavaScript Object Notation (JSON) Data Interchange Format. RFC 8259. https://doi.org/10.17487/ RFC8259

    2017

  2. [10]

    Ravi Chugh, Brian Hempel, Mitchell Spradlin, and Jacob Albers. 2016. Programmatic and direct manipulation, together at last. InPLDI. ACM, Santa Barbara, CA, USA, 341–354. https://doi.org/10.1145/2908080.2908103

    2016

  3. [11]

    Halbert, David Kurlander, Henry Lieberman, David Maulsby, Brad A

    Allen Cypher, Daniel C. Halbert, David Kurlander, Henry Lieberman, David Maulsby, Brad A. Myers, and Alan Turransky (Eds.). 1993.Watch what I do: programming by demonstration. MIT Press, Cambridge, MA, USA

    1993

  4. [12]

    Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008. Z3: An Efficient SMT Solver. InTACAS (Lecture Notes in Computer Science, Vol. 4963). Springer, Budapest, Hungary, 337–340. https://doi.org/10.1007/978-3-540-78800-3_24

    2008 doi

  5. [13]

    Rui Dong, Zhicheng Huang, Ian Iong Lam, Yan Chen, and Xinyu Wang. 2022. WebRobot: web robotic process automation using interactive programming-by-demonstration. InPLDI. ACM, San Diego, CA, USA, 152–167. https: //doi.org/10.1145/3519939.3523711

    2022

  6. [14]

    Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps. 2017. Component-based synthesis for complex APIs. InPOPL. ACM, Paris, France, 599–612. https://doi.org/10.1145/3009837.3009851

    2017

  7. [15]

    Margarida Ferreira, Ranysha Ware, Yash Kothari, Inês Lynce, Ruben Martins, Akshay Narayan, and Justine Sherry

  8. [16]

    2019.Extracting JSON Values with JsonPath: Document Processing for Java SE

    Jeff Friesen. 2019.Extracting JSON Values with JsonPath: Document Processing for Java SE. Apress Berkeley, CA, Berkeley, CA, USA, 299–322. https://doi.org/10.1007/978-1-4842-4330-5_10

    2019 doi

  9. [17]

    Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. 2017. Program Synthesis.Found. Trends Program. Lang.4, 1-2 (2017), 1–119. https://doi.org/10.1561/2500000010

    2017 doi

  10. [18]

    Zheng Guo, David Cao, Davin Tjong, Jean Yang, Cole Schlesinger, and Nadia Polikarpova. 2022. Type-directed program synthesis for RESTful APIs. InPLDI. ACM, San Diego, CA, USA, 122–136. https://doi.org/10.1145/3519939.3523450

    2022

  11. [19]

    Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, and Nadia Polikarpova. 2020. Program synthesis by type-guided abstraction refinement. InPOPL. ACM, New Orleans, LA, United States, 12:1–12:28. https://doi.org/10.1145/3371080

    2020 doi

  12. [20]

    Foster, and David Van Horn

    Sankha Narayan Guria, Jeffrey S. Foster, and David Van Horn. 2021. RbSyn: Type- and Effect-Guided Program Synthesis. InPLDI. ACM, Virtual, Canada, 344–358. https://doi.org/10.1145/3453483.3454048

    2021

  13. [21]

    Melham, Daniel Kroening, and John O’Leary

    Natasha Yogananda Jeppu, Thomas F. Melham, Daniel Kroening, and John O’Leary. 2020. Learning Concise Models from Long Execution Traces. InDAC. IEEE, San Francisco, CA, USA, 1–6. https://doi.org/10.1109/DAC18072.2020.9218613

    2020

  14. [22]

    Rajeev Joshi, Greg Nelson, and Keith Randall. 2002. Denali: A Goal-Directed Superoptimizer. InPLDI(Berlin, Germany). ACM, Beijing, China, 304–314. https://doi.org/10.1145/512529.512566

    2002

  15. [23]

    Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, and Yuval Yarom. 2023. CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives....

    2023 doi

  16. [24]

    Mitchell, and Brad A

    Toby Jia-Jun Li, Marissa Radensky, Justin Jia, Kirielle Singarajah, Tom M. Mitchell, and Brad A. Myers. 2019. PUMICE: A Multi-Modal Agent that Learns Concepts and Conditionals from Natural Language and Demonstrations. InUIST. ACM, New Orleans, LA, USA, 577–589. https://doi.org...

    2019

  17. [25]

    Xiang Li, Xiangyu Zhou, Rui Dong, Yihong Zhang, and Xinyu Wang. 2024. Efficient Bottom-Up Synthesis for Programs with Local Variables. InPOPL. ACM, London, UK, 1540–1568. https://doi.org/10.1145/3632894

    2024 doi

  18. [26]

    Benjamin Mariano, Ziteng Wang, Shankara Pailoor, Christian Collberg, and Işil Dillig. 2024. Control-Flow Deobfuscation using Trace-Informed Compositional Program Synthesis. InOOPSLA. ACM, Pasadena, CA, USA, 2211–2241. https: //doi.org/10.1145/3689789

    2024 doi

  19. [27]

    Wilcox, Eva Darulova, Dan Grossman, and Zachary Tatlock

    Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, and Zachary Tatlock. 2020. Synthesizing structured CAD models with equality saturation and inverse transformations. InPLDI. ACM, London, UK, 31–44. https://doi.org/10.1145/3385412.33860...

    2020

  20. [28]

    2025.Program Synthesis From Partial Traces (Software Artifact)

    Victor Nicolet and Margarida Ferreira. 2025.Program Synthesis From Partial Traces (Software Artifact). https: //doi.org/10.5281/zenodo.15047359

    2025 doi

  21. [29]

    Saswat Padhi, Elizabeth Polgreen, Mukund Raghothaman, Andrew Reynolds, and Abhishek Udupa. 2023. The SyGuS Language Standard Version 2.1. https://doi.org/10.48550/arXiv.2312.06001 arXiv:2312.06001 [cs.PL]

    2023 doi arXiv

  22. [30]

    Fink, Rodric M

    Cosmin Radoi, Stephen J. Fink, Rodric M. Rabbah, and Manu Sridharan. 2014. Translating imperative code to MapReduce. InOOPSLA. ACM, Portland, OR, USA, 909–927. https://doi.org/10.1145/2714064.2660228

    2014

  23. [31]

    Eric Schkufza, Rahul Sharma, and Alex Aiken. 2013. Stochastic superoptimization. InASPLOS. ACM, Houston, Texas, USA, 305–316. https://doi.org/10.1145/2451116.2451150

    2013

  24. [32]

    Jiasi Shen and Martin C. Rinard. 2019. Using active learning to synthesize models of applications that access databases. InPLDI. ACM, Phoenix, AZ, USA, 269–285. https://doi.org/10.1145/3314221.3314591

    2019

  25. [33]

    Richard Shin, Illia Polosukhin, and Dawn Song. 2018. Improving Neural Program Synthesis with Inferred Execution Traces. InNeurIPS. Curran Associates, Inc., Montréal, Canada, 8931–8940. https://proceedings.neurips.cc/paper/2018/ hash/7776e88b0c189539098176589250bcba-Abstract.html

    2018

  26. [34]

    Emina Torlak and Rastislav Bodík. 2014. A lightweight symbolic virtual machine for solver-aided host languages. In PLDI. ACM, Edinburgh, UK, 530–541. https://doi.org/10.1145/2594291.2594340

    2014

  27. [35]

    Eelco Visser. 2001. A Survey of Rewriting Strategies in Program Transformation Systems.Electronic Notes in Theoretical Computer Science57 (2001), 109–143. https://doi.org/10.1016/S1571-0661(04)00270-1

    2001 doi

  28. [36]

    Wong, Tanvi Wagle, Srinivas Narayana, and Anirudh Sivaraman

    Qiongwen Xu, Michael D. Wong, Tanvi Wagle, Srinivas Narayana, and Anirudh Sivaraman. 2021. Synthesizing safe and efficient kernel extensions for packet processing. InSIGCOMM. ACM, Virtal (online), 50–64. https://doi.org/10. 1145/3452296.3472929

    2021

  29. [37]

    api": <THE API NAME>,

    Kuat Yessenov, Ivan Kuraj, and Armando Solar-Lezama. 2017. DemoMatch: API discovery from demonstrations. In PLDI. ACM, Barcelona, Spain, 64–78. https://doi.org/10.1145/3062341.3062386 Proc. ACM Program. Lang., Vol. 9, No. PLDI, Article . Publication date: June 2025. A Benchmar...

    2017

  30. [2024]

    Reverse-Engineering Congestion Control Algorithm Behavior. InIMC. ACM, Madrid, Spain, 401–414. https: //doi.org/10.1145/3646547.3688443

Pith tools

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