News

  • See “Time & Location” below.

Basic Information

  • Instructor: Woosuk Lee
    • Office Location: Rm#403, Eng. Bldg 3
    • Telephone: 031-400-1031
    • Email: woosuk at hanyang.ac.kr
    • Office Hours: Wednesday 13:00 - 15:00
  • Time & Location
    • Wednesday 15:00 - 17:15 @ Y317-0306

References

  • The course textbook: Program Synthesis by Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh

Slides & Course Schedule (tentative)

  • Course overview & Introduction to program synthesis: pdf
  • Syntax-guided synthesis: pdf
  • Enumerative search: pdf
  • Search prioritization: pdf
  • Representation-based search: pdf
  • Bidirectional search: pdf
  • Stochastic search: pdf
  • Constraint-based search:pdf
  • Type-driven synthesis: pdf
  • Deductive synthesis: pdf
  • Neurosymbolic synthesis
  • Applications of synthesis: pdf

Grading

  • Student presentation: 30%
  • Project: 60%
  • Attendance: 10%

Student presentation

Project ideas

Reading Material

Reading material related to the lesson

  • Syntax-guided synthesis
    • Syntax-guided synthesis. FMCAD’13
    • Dimensions in Program Synthesis. PPDP’10
  • Enumerative search
    • Scaling Enumerative Program Synthesis via Divide and Conquer. TACAS’17
    • Scaling Up Superoptimization. ASPLOS’16
    • Inductive Program Synthesis Guided by Observational Program Similarity. OOPSLA’23
    • Oriented Metrics for Bottom-Up Enumerative Synthesis. POPL’26
    • A Concurrent Approach to String Transformation Synthesis. PLDI’25
  • Search prioritization
    • Distance-Guided Search in Program Synthesis with Imperfect LLM Solutions. ICSE’26
    • Accelerating Search-Based Program Synthesis using Learned Probabilistic Models. PLDI’18
    • Just-in-Time Learning for Bottom-Up Enumerative Synthesis. OOPSLA’20.
    • Guided Tensor Lifting. PLDI’25
  • Representation-based search
    • Automating string processing in spreadsheets using input-output examples. POPL’11
    • FlashMeta: a framework for inductive program synthesis. OOPSLA’15
    • Program synthesis using abstraction refinement. POPL’18
    • Component-based synthesis for complex APIs. POPL’17
    • egg: Fast and extensible equality saturation. POPL 2021
    • Equality Saturation Theory Exploration à la Carte. OOPSLA 2023
    • Better Together: Unifying Datalog and Equality Saturation. PLDI’23
    • Guided Equality Saturation. POPL’24
  • Bidirectional search
    • Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling. POPL 2026
    • Inductive Program Synthesis via Iterative Forward-Backward Abstract Interpretation. PLDI 2023
    • Combining the Top-down Propagation and Bottom-up Enumeration for Inductive Program Synthesis. POPL 2021
    • Web Data Extraction Using Hybrid Program Synthesis: A Combination of Top-down and Bottom-up Inference. SIGMOD 2020
    • Synthesizing Geometry Constructions. PLDI 2011
    • Scaling up Superoptimization. ASPLOS 2016
  • Constraint-based search
    • Oracle-guided component-based program synthesis. ICSE’10
    • Program synthesis using conflict-driven learning. PLDI’18
  • Stochastic search
    • Stochastic program optimization. CACM’16
    • Adaptive Restarts for Stochastic Synthesis. PLDI’21
    • Recursive Program Synthesis using Paramorphisms. PLDI’24
  • Type-driven synthesis
    • Inductive Synthesis of Structurally Recursive Functional Programs from Non-Recursive Expressions. POPL’23
    • Type-and-example-directed program synthesis. PLDI’15
    • Example-directed synthesis: a type-theoretic interpretation. POPL’16
    • Synthesizing Data Structure Transformations from Input-Output Examples. PLDI 2015
    • Program synthesis from Polymorphic Refinement Types. PLDI’16
  • Deductive synthesis
    • Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV’15
    • Reconciling enumerative and deductive program synthesis, PLDI’20
  • Neurosymbolic synthesis
    • Scallop: A Language for Neurosymbolic Programming. PLDI’23
    • Active Learning for Neurosymbolic Program Synthesis. OOPSLA’25
    • ImageEye: Batch Image Processing Using Program Synthesis. PLDI’23
    • ChopChop: a Programmable Framework for Semantically Constraining the Output of Language Models. POPL’26
    • Type-Constrained Code Generation with Language Models. PLDI’25
  • Applications of synthesis
    • Lightweight Concolic Testing via Path-Condition Synthesis for Deep Learning Libraries. ICSE’25
    • Identifying Potential Timing Leakages from Hardware Design with Precondition Synthesis. ESORICS’25
    • PBE-Based Selective Abstraction and Refinement for Efficient Property Falsification of Embedded Software. FSE’24
    • Simplifying Mixed Boolean-Arithmetic Obfuscation by Program Synthesis and Term Rewriting. CCS’23
    • Optimizing homomorphic evaluation circuits by program synthesis and term rewriting, PLDI’20
    • Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits, CAV’16
    • FlashExtract: a framework for data extraction by examples. PLDI’14
    • On the Fly Synthesis of Edit Suggestions, OOPSLA’19
    • From Batch to Stream: Automatic Generation of Online Algorithms. PLDI’24
    • Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers. POPL’26
    • Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis. PLDI’24
    • Program Synthesis From Partial Traces. PLDI’25
    • Automated policy synthesis for system call sandboxing. OOPSLA’20

      Some part of the slides is based on the lecture notes of similar courses by

    • Nadia Polikarpova’s course at UCSD on program synthesis
    • Armando Solar-Lezamma’s course1 and course2 on program synthesis