Imagine you’re a system administrator managing a complex cloud deployment. Day after day, you perform the same tedious sequence before leaving work: find, in the list of active computing instances, those no longer used by your team, select them, and click “Stop instances”. Then, after a few seconds, you check whether they have already stopped; if not, you click “Force stop instances”. Dozens of clicks through web interfaces like the one below, over and over again.

What if, after a few days of silently watching you perform this task, the system could write the code to automate it for you, without you having to explain a single thing?

This is what the technique introduced in our paper Program Synthesis from Partial Traces (PLDI 2025) does!

Our system, Syren , synthesizes general-purpose automation scripts from execution traces: the logs a system already records while its user performs a task by hand. Unlike prior approaches to program synthesis, which require users to actively describe what they want through formal specifications, input-output examples, or natural language, Syren works from data users already have. The challenge is that these traces are partial: they record the user’s interactions with the system, but not the data transformations or control-flow decisions the user computes in their head. Syren ’s key novelty is recovering these hidden computations: it starts from a trivial program that merely replays the traces, then applies program rewrites, backed by synthesis from input-output examples, to uncover the hidden logic and generalize the program into a readable script.

Program Synthesis

For as long as we’ve had programming languages to automate our daily tasks, computer scientists have been thinking of ways to automate writing code itself. That’s the premise of program synthesis : the task of automatically generating executable code from a high-level specification. The journey began with logical formulations as specifications ( Manna & Waldinger, TOPLAS 1980 ). These precise, mathematical specifications completely define the desired program’s behavior, but they are expressed in a formal language that requires significant expertise to write. Then came input-output examples, popularized by tools like Microsoft Excel’s FlashFill ( Gulwani, POPL 2011 ): “give me a program that for input X outputs Y.” Examples are much simpler, but in practice, they still require expertise and multiple iterations. They are inherently ambiguous because multiple programs can generate the same set of examples. This means the user has to cover specific corner cases and inspect the output for any unexpected behavior. Recently, with advancements in large language models (LLMs), natural language emerged as the go-to specification ( Chen et al., 2021 ), making programming more accessible to non-experts than ever. But this comes at a cost: unlike logical formulas and examples, it’s not clear how to verify that a program satisfies a natural-language specification.

All these synthesis specifications have something in common: they’re active specifications. They require users to explicitly articulate what they want, often through multiple rounds of clarification. With Syren , we propose using passive specifications instead: synthesizing programs from data users already have, requiring no additional knowledge or effort. Specifically, we synthesize programs from execution traces, the digital breadcrumbs left behind by every modern computing system to help us trace back its computations. These traces, whether sequences of API calls, network messages between servers, or system call logs, capture not just the everyday behaviors of systems but also corner cases and execution subtleties. They are already used for monitoring, debugging, and auditing, so why not use them to synthesize automations for hand-executed tasks in these systems, or optimized versions of existing routines?

Synthesis from Partial Traces

The main challenge in synthesizing a program from real-world traces is that they provide only a partial view of what’s happening. These traces record only some of the actions the user takes; for example, operations that get billed, or side-effecting executions that interact with external resources, such as network calls or file writes. They lack information about intermediate steps that may transform data internally or affect control flow.

Revisiting the example from the beginning: when the admin stops unused instances, every time they click a button in the visual console, the console calls a specific API method under the hood, and that call gets recorded. But the admin’s decision to potentially force some computing instances to stop after a while, depending on each instance’s status, is not recorded. This “computation” happens only in the user’s head. To automate the task, we need to automate both sides of the computation: the visible API method calls and the hidden computations that the user executes manually. Inferring these hidden functions poses a significant challenge for synthesis, but without them, the task can’t be automated correctly.

For the purpose of this work, we define a trace as the sequence of API methods invoked during a single execution of a task. The traces include the method name, inputs, and outputs for all API calls. Syren synthesizes programs from these partial traces by inferring both control flow and non-trivial hidden functions without additional user input.

Syren ’s Synthesis Procedure

Example Execution

Performing the example cloud computing task described above in the Amazon Web Services (AWS) console produces logs that show the sequence of underlying API calls made by the system. These logs can be input as traces into Syren for synthesis. Below is an example trace of the execution of this task for a single computing instance with ID "i-12345" , which we call Trace #1:

(
 ec2.StopInstances("InstanceIds": ["i-12345"], "force": false),
 { ... }
)


(
 ec2.DescribeInstanceStatus("InstanceIds": ["i-12345"]),
 {"InstanceState": "stopped", ...}
)

Trace #1 contains two API calls, ec2.StopInstances and ec2.DescribeInstanceStatus , each represented as a pair in parentheses: the first element of the pair shows the API method name and its inputs (the request parameters), and the second shows its output (the response). In the output of ec2.DescribeInstanceStatus , the instance is showing as "stopped" . That is the goal; the system admin’s task is complete.

The next day, the system admin could execute the same task on instance "i-54321" and generate the following trace (Trace #2):

(
 ec2.StopInstances("InstanceIds": ["i-54321"], "force": false),
 { ... }
)


(
 ec2.DescribeInstanceStatus("InstanceIds":["i-54321"]),
 {"InstanceState": "stopping", ...}
)


(
 ec2.StopInstances("InstanceIds": ["i-54321"], "force": true),
 { ... }
)

In this second execution of the task, ec2.DescribeInstanceStatus shows the current status of the instance as "stopping" (not "stopped" ), so there is a second call to ec2.StopInstances with force set to true .

When working with traces like these, there’s always a trivial solution: a program that exactly reproduces the input traces. But users don’t want this brittle reproduction; they want a program that generalizes beyond the examples they’ve shown. Our cloud administrator doesn’t need a script that stops the exact computing instances they’ve stopped in the past; they need one that takes a list of instance IDs as a parameter, handling the repetitive parts automatically while still letting them provide the essential information. This trivial program is still useful to Syren : it serves as the starting point of our synthesis, which progressively makes it more general and readable.

Initial Program

Syren ’s programs are written in a programming language formally defined in the paper . Its syntax and semantics are similar to those of commonly used imperative languages, such as Python, so users with programming backgrounds can read and edit Syren programs, and these programs can be easily compiled to other languages.

We build the initial program by branching the execution on the value of a fresh integer variable, br , which is received as an input parameter, and replaying each trace on a different branch. In Syren ’s syntax, we explicitly represent the program’s input parameters on the first line, preceded by a λ . So, λ br. in the first line means the program takes as input one parameter, br . In the initial program, the sequence of API calls is reproduced exactly as shown in the traces, and all values are hard-coded constants. For the two traces shown before, Syren ’s initial program would be:

λ br.
if br == 1 {
  let x_1_1 = ec2.StopInstances(instanceIds=["i-12345"], force=false)
  let x_1_2 = ec2.DescribeInstanceStatus(instanceIds=["i-12345"])
} else {
  let x_2_1 = ec2.StopInstances(instanceIds=["i-54321"], force=false)
  let x_2_2 = ec2.DescribeInstanceStatus(instanceIds=["i-54321"])
  let x_2_3 = ec2.StopInstances(instanceIds=["i-54321"], force=true)
}

This program will reproduce Trace #1 if the parameter br is set to 1 and Trace #2 otherwise. In practice, Syren uses more than two traces, so there are more conditionals in this top-level if-else chain.

This initial program is correct by construction: for each trace the user provided, there exists an input for which the program reproduces it. But it doesn’t generalize beyond the traces, so, from here, Syren applies a series of optimizing rewrites : compiler-like, correctness-preserving transformations that make the program more general, more readable, and thus closer to the ideal program we want to return to the user.

Rewriting the Original Program

Syren ’s first rewrites replace the instance IDs, which are constants hard-coded repeatedly in multiple calls, with a new input parameter to the script, i_0 . They also pull the first call to ec2.StopInstances and the call to ec2.DescribeInstanceStatus out of the if-statement, since they are identical in both branches. These rewrites reduce the program size and eliminate repeated API calls, two of Syren ’s optimization goals. The program below is the result of these transformations.

λ br.
if br == 1 {
  let x_1_1 = ec2.StopInstances(instanceIds=["i-12345"], force=false)
  let x_1_2 = ec2.DescribeInstanceStatus(instanceIds=["i-12345"])
} else {
  let x_2_1 = ec2.StopInstances(instanceIds=["i-54321"], force=false)
  let x_2_2 = ec2.DescribeInstanceStatus(instanceIds=["i-54321"])
  let x_2_3 = ec2.StopInstances(instanceIds=["i-54321"], force=true)
}

λ br, i_0.
let x_1 = ec2.StopInstances(instanceIds=i_0, force=false)
let x_2 = ec2.DescribeInstanceStatus(instanceIds=i_0)
if !(br == 1) {
  let x_2_3 = ec2.StopInstances(instanceIds=i_0, force=true)
}

The program above still depends on br , an artificial variable with no real semantic meaning: the conditional !(br==1) decides whether the second, forced call to ec2.StopInstances runs. Syren could remove it as it did the instance IDs, by introducing a new input parameter, in this case a Boolean that the user would set to request the forced stop. But that is not what happened in the example task: the administrator decided whether to force the stop based on the outcome of the previous call to ec2.DescribeInstanceStatus . If the instance does not show as "stopped" yet, they force it.

Syren always tries to infer these hidden data dependencies on previous instructions in the script before defaulting to introducing new parameters. So, in the final rewrite of this example, it replaces !(br==1) with the output of a new function φ , a stand-in for the computation the user performed in their head. Since we don’t know what previous information the user relied on, φ takes as input all variables in scope at this point in the program. φ remains undefined for now, so we declare the program is parametric on its implementation in the first line with Λ φ. .

λ br, i_0.
let x_1 = ec2.StopInstances(instanceIds=i_0, force=false)
let x_2 = ec2.DescribeInstanceStatus(instanceIds=i_0)
if !(br == 1) {
  let x_2_3 = ec2.StopInstances(instanceIds=i_0, force=true)
}

Λ φ. λ i_0.
let x_1 = ec2.StopInstances(instanceIds=i_0, force=false)
let x_2 = ec2.DescribeInstanceStatus(instanceIds=i_0)
let c = φ(i_0, x_1, x_2)
if c {
  let x_2_3 = ec2.StopInstances(instanceIds=i_0, force=true)
}

Example-Based Synthesis of Hidden Functions

Of course, this program is only useful if we can provide an implementation f for φ for which the program can perform the task. This is where example-based synthesis comes in. During the rewrite process, we maintain a mapping from program identifiers to their corresponding values in the traces. Then, we use these mappings to compute a set of input-output constraints that f must satisfy, and feed them to an off-the-shelf example-based synthesizer to generate an implementation of φ . Syren supports two such synthesizers: Rosette ( Torlak et al., Onward! 2013 ) and cvc5 ( Barbosa et al., TACAS 2022 ).

Looking side by side at the program above and the traces it was built from, we can read off the values φ ’s arguments take in each trace: i_0 is the instance ID, and x_1 and x_2 are the responses of the two API calls, as annotated in the constraints below. The output of φ is a Boolean value that indicates whether the instance has not yet stopped and needs to be forced to stop: false for the first trace and true for the second.

So, for the traces and program in this example, we know f must be such that:

f(["i-12345"], /* parameter i_0 */
  {"StoppingInstances": [...], "ResponseMetadata": {...}}, /* response from StopInstances, x_1 */
  {"InstanceState" : "stopped", ...} /* response from DescribeInstanceStatus, x_2 */
) = false

for Trace #1, and

f(["i-54321"], /* parameter i_0 */
  {"StoppingInstances": [...], "ResponseMetadata": {...}}, /* response from StopInstances, x_1 */
  {"InstanceState" : "stopping", ...} /* response from DescribeInstanceStatus, x_2 */
) = true

for Trace #2.

From these constraints, the synthesizer generates the simplest logical expression that fits the behavior in the traces, giving the following implementation f for φ :

f := (i_0, x_1, x_2) -> x_2.InstanceState != "stopped"

Substituting f for φ yields a program that is correct by construction. Since f uses only its last input, we simplify it to take just x_2 .

Λ φ. λ i_0.
let x_1 = ec2.StopInstances(instanceIds=i_0, force=false)
let x_2 = ec2.DescribeInstanceStatus(instanceIds=i_0)
let c = φ(i_0, x_1, x_2)
if c {
  let x_2_3 = ec2.StopInstances(instanceIds=i_0, force=true)
}

λ i_0.
let _ = ec2.StopInstances(instanceIds=i_0, force=false)
let x_2 = ec2.DescribeInstanceStatus(instanceIds=i_0)
let c = f(x_2)
if c {
  let _ = ec2.StopInstances(instanceIds=i_0, force=true)
}
where
f := (x) -> x.InstanceState != "stopped"

This final program executes the task described at the beginning!

Beyond the Example: Search over a Library of Rewrites

Syren ’s library of rewrite rules includes many more rules than the ones used in the example above. Rewrites fall into two categories:

Refinement rules are simple structural transformations. These might lift identical statements out of conditionals or replace constants with parameters. They are correctness-preserving by construction and don’t require synthesis. They uncover the program’s control flow in a way that explains the observed traces.

Synthesis rules introduce hidden functions. They replace expressions with fresh calls to unknown functions \(\varphi\), which are later synthesized from input-output examples. These rules apply only if a valid implementation of \(\varphi\) that preserves trace behavior exists.

All rewrite rules are defined as patterns. As an example, below is the definition of the first rewrite rule shown in the example above, which extracts an identical sequence of instructions \(\mathcal{R}\) from both the then-branch and the else-branch of a conditional. \(\mathcal{R}\), \(\mathcal{S}\), \(\mathcal{T}\), \(\mathcal{U}\), and \(\mathcal{V}\) are arbitrary sequences of instructions in the program.

When the program Syren is considering has the structure on the left, the rule applies, and the program is rewritten with the structure on the right. The application of synthesis rules is subject to an additional constraint: synthesizing any required hidden functions. When we can’t find an implementation for \(\varphi\), whether it is used in a control-flow conditional or as an input to a function call, that indicates the rewrite is misguided.

At any stage of the rewrite process, many rules can be applied to the program, too many to try them all. Instead, Syren performs a cost-directed search, using a cost function that penalizes undesirable program characteristics. The cost functions in Syren prefer smaller, more general, and human-readable programs. In the paper, we implement two concrete cost functions that illustrate how different notions of “simplicity” yield different outcomes.

The first, \(\chi_{\mathrm{syn}}\), follows the widely used Occam’s razor principle and favors purely syntactic simplicity: it assigns a weighted penalty to every statement, every parameter, and every use of the synthetic variable br . \(\chi_{\mathrm{syn}}\) produces a fine-grained score that distinguishes most programs from one another, giving the search a clear signal at nearly every step.

Syren implements a second cost function, \(\chi_{\mathrm{T}}\), which takes a more semantic view of the programs: rather than counting syntactic elements, it measures how much each API call is reused across the input traces. A statement executed many times, such as an API call inside a loop shared across traces, contributes more reuse and therefore incurs lower \(\chi_{\mathrm{T}}\) cost than the same calls written out redundantly in separate branches. It also penalizes branches that only reproduce a single input trace, treating them as corner cases that suggest the program has not yet generalized. In practice, \(\chi_{\mathrm{T}}\) is worse at directing the search than \(\chi_{\mathrm{syn}}\), because it is coarser: more programs have the same score. With either cost function, Syren synthesizes programs for a similar number of tasks, but \(\chi_{\mathrm{syn}}\) generates programs that are easier to read.

The cost function does more than rank programs after applying rewrites. It actively controls which rewrites to apply at every step of the search. Syren treats the two types of rewrites differently. At each step, it first scans all applicable refinement rules and greedily applies the one that yields the greatest cost reduction, repeating this until no refinement rule can lower the cost further. Only then does it consider synthesis rules, again selecting the most cost-reducing one and invoking the example-based solver to check whether a valid implementation exists for any newly introduced computation. This ordering exhausts the cheap structural rewrites first, so the solver is called as sparingly as possible. As with the cost function itself, Syren ’s source code provides predefined search strategies but allows users to define their own.

Final Thoughts

Syren is, to our knowledge, the first approach to synthesizing programs that combine side-effecting API calls, control flow, and hidden pure functions purely from execution traces: no annotations, no natural language, no hand-crafted examples.

In the paper , we showcase Syren ’s practical applicability. We evaluate it on 54 real-world tasks, including cloud automation, filesystem manipulation, and document editing scripts, drawn from custom tasks, existing AWS Automation Runbooks , Blink Automations , and related work from Guo et al. at PLDI 2022 . The underlying example-based synthesizer generates non-trivial data transformations that allow Syren to uncover more intricate computations that are not visible in the traces. Syren introduces control structures like if-then-else conditionals and retry-until loops, and synthesizes correct, human-meaningful scripts for 39 of the 54 tasks in under 5 minutes.

Though powerful, the synthesis of data transformations is Syren ’s main bottleneck: when the hidden functions require complex manipulation of JSON data, the underlying example-based synthesizer can fail to find the right expression, either due to the time limit imposed or because the required computation is not in the language of JSON operations we use. Improving Syren ’s performance would require more specialized grammars or solvers for this domain. There is another limitation worth acknowledging beyond performance: the quality of Syren ’s programs depends heavily on having sufficiently rich and diverse traces. If the traces don’t capture the data needed to compute a value, Syren falls back to treating that value as an input parameter. Two very similar traces may provide too little signal for the synthesis-by-example solver to distinguish the right hidden function from a degenerate one. Looking ahead, there are natural extensions to explore. Real-world traces are recorded from humans, and humans are inconsistent. An action a user took once in an unusual mood may not reflect the general pattern they want to automate, but Syren currently tries to explain every trace it’s given, treating all of them as equally intentional. A natural extension would be allowing Syren to identify and discard outlier traces, synthesizing a program that fits the majority of the observed behavior rather than demanding a perfect explanation for all of it.

As systems become more API-driven and observability tooling improves, the resulting raw logs become more abundant. Syren takes a step towards a future where that data doesn’t just sit in a dashboard waiting to be analyzed, but actively gets turned into automation. Instead of asking users to articulate what they want, we can just watch what they do.