CS292C-11: Computer-Aided Reasoning for Software
Lecture 11: Program Synthesis: From Specs to Code

by Yu Feng

Why Should I Care?
Less hand coding
Focus on problem solving instead
Machine-checked guarantees
Creates safer software
Super-human optimization
Souper / LLVM improvements
Enhanced auto-completion
Copilot + constraints
Roadmap Today
1
The big-picture taxonomy
Understanding synthesis approaches
2
Deductive synthesis
With practical example
3
Inductive/PBE synthesis
With practical example
4
Real-world wins
Industry success stories
5
Research frontiers
Project hints included
Synthesis in the Real World: DARPA MUSE
In 2014, DARPA launched the Mining and Understanding Software Enclaves (MUSE) program to revolutionize how we create, maintain, and verify software.
Mining Big Code
Creating a massive database of open-source code to learn patterns and extract knowledge about software behavior.
Automatic Bug Finding
Developing techniques to automatically detect and fix vulnerabilities by analyzing millions of code examples.
Program Synthesis
Automatically generating code from specifications, reducing engineering effort while increasing reliability.
MUSE demonstrated program synthesis as a transformative technology that could dramatically improve software productivity, security, and correctness at scale.
Synthesis Styles (cheat-sheet)
Deductive in 20 seconds
Goal
Derive program from specification: {P} Program {Q} where P is precondition and Q is postcondition
Process
Apply formal rules of inference (like weakest precondition) to transform specifications into executable code
Result
Program and correctness proof are developed simultaneously through logical derivation
Guarantee
Provably correct implementation that satisfies specification with mathematical certainty
Manna, Zohar, and Richard Waldinger. "A deductive approach to program synthesis." ACM Transactions on Programming Languages and Systems (TOPLAS), 1980
{ x=A ∧ y=B } ? { x=B ∧ y=A }
Concrete Example – XOR Swap
Deductive synthesis transforms this specification into a provably correct implementation:
The synthesis process determines each operation by analyzing how to transform the state to meet postconditions while maintaining correctness.
Key insight: XOR (⊕) has the property that (A⊕B)⊕B = A, which allows us to swap variables without using a temporary variable.
XOR Swap (Correctness)
{ x = A ∧ y = B }
x := x XOR y;   // S1
y := x XOR y;   // S2
x := x XOR y;   // S3
{ x = B ∧ y = A }
Derived by equational reasoning. Bit-trick emerges automatically.
Initialisation: spec → invariant via assignment rules
Preservation: each step proven with Hoare assignment rule
Composition: {P} S1;S2;S3 {Q} by sequencing
Outcome: program synthesised and fully verified, demonstrating deductive synthesis in three proof-guided refinements.
Polikarpova's Synquid: Maximum Element
Finding the maximum value in a list using refinement types in Synquid:
maxList :: xs:{List Int  | len xs > 0} -> {v:Int | v ∈ xs && (∀y ∈ xs. v ≥ y)}
Synthesis Process:
Synquid follows a top-down search to synthesize the implementation:
  1. Start: Need an Int that satisfies the output refinement
  1. Strategy: Break down by pattern-matching on the input list xs
  1. Case 1 (Base): xs = Cons h [] → return h (type-checker validates this immediately)
  1. Case 2 (Recursive): xs = Cons h t where len t ≥ 0 - Recursively synthesize m = maxList t - Choose: if h ≥ m then h else m - Solver automatically verifies this satisfies all refinements
The synthesis engine proves correctness at each step, ensuring the implementation meets the specification with mathematical certainty.
Polikarpova, Nadia, et al. "Synquid: Synthesizing Programs from Liquid Types." PLDI, 2016.
Synthesized Implementation
maxList xs =
  case xs of
    Cons h Nil -> h
    Cons h t ->
      let m = maxList t in
      if h >= m then h else m
Key take-aways
  • Refinement types = deductive spec → synthesis is type-driven.
  • Solver (Horn-SMT) prunes invalid paths → minutes to seconds even for recursive data.
  • Illustrates Nadia Polikarpova's insight: verification infrastructure doubles as synthesis engine.
What are the cons of deductive synthesis?
Deductive Synthesis — Pros & Cons in Practice
👍 Pros
  • Correct-by-construction — no post-verification needed
  • Mathematical certainty — formal guarantees throughout
  • Excellent for critical code — security, aviation, medical
  • Reveals insights — elegant algorithms emerge naturally
👎 Cons
  • Requires complete formal spec — high expertise barrier
  • Computationally intensive — scales poorly with complexity
  • Limited to specific domains — not general-purpose
  • Tools require interactive guidance — not fully automated
Inductive Synthesis — One-Slide Snapshot
Key idea: Bias + Examples ⇒ Program
Bias
A carefully chosen domain-specific language (DSL) that limits what can be expressed
Examples
I/O pairs, unit tests, or traces supplied by the user
Instead of proving a program correct, inductive synthesis generalizes from concrete examples to discover programs
Typical workflow:
  1. Choose a DSL – balances expressiveness with search tractability
  1. Generate candidates – enumerate or probabilistically sample programs, smallest first
  1. Quick-check – execute on examples; reject on first mismatch, pruning huge swaths of the search tree
  1. Symbolic pruning – invoke a solver to eliminate infeasible paths without explicit enumeration
FlashFill: Programming By Example
Microsoft's Smart Data Transformation
FlashFill automatically detects patterns in your data and generates transformation programs from just a few examples. This Excel feature learns string manipulation programs on-the-fly, eliminating the need for complex formulas or macros.
No Programming Required
Users simply provide a few examples of the desired output, and FlashFill synthesizes the appropriate transformation program.
Instant Pattern Recognition
Identifies complex string patterns and data regularities in milliseconds, saving hours of manual work.
Handles Complex Transformations
Capable of name formatting, data extraction, date standardization, and multi-step transformations.
Real-world impact: FlashFill saves millions of work-hours annually across industries by automating tedious data cleaning tasks that previously required custom programming.
“FlashFill: Programming by Example for Text Processing” — Sumit Gulwani, PLDI 2011
Concrete PBE Example – Flash-Fill
FlashFill learns string manipulation patterns from just a few examples, automatically generating the transformation for the entire dataset:
Before (User Input)
User provides just 2 examples of the desired transformation
After (FlashFill Completes)
FlashFill synthesizes the pattern: Last Name + ", " + First Initial + "."
FlashFill has automatically detected the pattern and applied it to the entire dataset without requiring users to write a single line of code or formula.
Behind the Scenes: FlashFill's DSL
// FlashFill's Domain Specific Language (DSL)
P        ::= Concat(f₁, f₂, ..., fₖ)         // Program is a concatenation of expressions
f        ::= ConstStr(s)                      // Constant string literal
           | SubStr(v, pₗ, pᵣ)                // Substring from input column v
pₗ, pᵣ   ::= Pos(v, R₁, R₂, k)               // Position defined by regex match
           | ConstPos(k)                      
// Example: Name formatting (Smith, J.)
Concat(
  SubStr(v₂, ConstPos(0), ConstPos(∞)),      // Last Name (column 2)
  ConstStr(", "),                             // Constant string ", "
  SubStr(v₁, ConstPos(0), ConstPos(1)),      // First character of First Name (column 1)
  ConstStr(".")                               // Constant string "."
)
  1. Analyzes input-output examples to identify patterns
  1. Searches through possible DSL expressions that satisfy the examples
  1. Ranks candidate programs by simplicity and generalizability
  1. Selects the highest-ranked program to apply to the remaining data
The synthesis algorithm uses version space algebra to efficiently represent and search through the space of possible programs, pruning invalid candidates early to maintain interactive response times.
Spectrum of Inductive Synthesis
Inductive synthesis techniques vary across multiple dimensions, with different approaches offering unique trade-offs in performance, completeness, and scalability.
Search Strategies
BFS/DFS
Systematic enumeration of programs in DSL, often with prioritization heuristics
SMT-based
Encoding synthesis problem as constraints to leverage SMT solver capabilities
ML-guided/MCMC
Learning-based approaches to predict likely program structures
Pruning Strategies
CEGIS
Counterexample-Guided Inductive Synthesis: iterative refinement using counterexamples
Conflict-driven
Learning from failures to avoid exploring similar incorrect programs
Correct-by-construction
Building programs that satisfy specifications by design, without verification
Most practical synthesis tools combine multiple strategies for better performance, often using ML to guide search and CEGIS to validate solutions efficiently.
Pruning: CEGIS
Synthesize
Generate candidate from spec and counter-examples
Verify
Check if candidate meets spec
Counter-example
Find case where candidate fails
Iterate
Feed counter-example back to synthesizer
SAT/SMT used on both sides – ties back to previous lectures
Solar-Lezama, Armando, et al. "Combinatorial sketching for finite programs." ASPLOS'2006.
CEGIS by Example
Let's walk through a concrete CEGIS example inspired by Solar-Lezama's sketch paper:
Initial Sketch
max(a,b) = { return ??; }
Programmer provides partial implementation with "holes" (??) to be filled
Synthesis Attempt
Generate candidate: max(a,b) = { return a; }
Solver tries a simple solution first
Counterexample
Found: max(2,5) = 2 ≠ 5
Verifier identifies a case where a < b
4
Final Synthesis
max(a,b) = { return (a > b) ? a : b; }
Generator produces correct implementation that passes all cases
The CEGIS loop iteratively refines the solution by learning from counterexamples. With each iteration, the synthesizer adds constraints to avoid previous failures until finding a solution that works for all inputs.
E-Graphs By Example
An E-graph is a data structure that efficiently represents many equivalent expressions. Let's use a concrete example with basic algebraic expressions:
(x + y) * 2    // Original expression
x * 2 + y * 2  // Distributive property 
2 * x + 2 * y  // Commutative property
2 * (x + y)    // Factoring
In an E-graph, all these expressions are stored in a single structure that recognizes they're equivalent. Instead of choosing one "best" form immediately, an E-graph maintains all equivalences simultaneously.
When optimization tools like "egg" (equality saturation) use E-graphs, they can:
  • Discover multiple equivalent ways to express the same computation
  • Apply various rewrite rules in any order without committing to a specific path
  • Extract the optimal expression according to a cost function (e.g., fewest operations)
E-Graph Equality Saturation (EGG)
EGG is a Rust library and approach for program synthesis that uses equality graphs (e-graphs) to efficiently represent and reason about equivalent program expressions.
Equality Saturation
Instead of applying rewrites sequentially, EGG applies all possible rewrites simultaneously, building a compact representation of the entire space of equivalent programs.
E-Graphs
Specialized data structures that efficiently represent many equivalent expressions, avoiding the combinatorial explosion that plagues traditional synthesis approaches.
Optimization
Enables efficient search for optimal program implementations by applying cost functions to select the best equivalent expression from the e-graph.
Advantages
Avoids getting stuck in local optima, provides formal guarantees, and scales to complex program transformations that would be intractable with traditional synthesis methods.
EGG extends equality saturation techniques to make them more accessible and efficient for program optimization, synthesis, and verification tasks across various domains.
Inductive Synthesis: Pros & Cons
👍 Strengths
Little spec burden
Users provide a few examples or tests, not full formal specifications
Friendly to end-users
Powers tools like Excel Flash-Fill and low-code platforms
Rapid feedback loop
Counter-examples or new examples refine the synthesis process
Domain-scalable
Can be applied across various application domains
👎 Limitations
Generalisation risk
Program may pass examples yet be wrong on unseen inputs
DSL design bottleneck
Too rich → search explodes; too weak → can't express solution
Ranking ambiguity
Many programs satisfy small example sets; choosing "best" is heuristic
Spec incompleteness
Examples often fail to fully characterize desired program behavior
What's Next?
1
Conflict-driven Synthesis in Details
Exploring advanced techniques that leverage conflicts to guide the synthesis process and improve efficiency
2
Final Project Illustrations
Examining concrete examples and implementation strategies for your synthesis projects
3
Program Repair
Learning how synthesis techniques can be applied to automatically fix bugs and improve existing code