News

  • No class on May 6th (Children’s Day)
  • No class on March 18th
  • 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 10:00 - 12:00
  • Time & Location
    • Monday 14:00 - 17:00 @ Rm 416, 4th Eng Bldg.

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 pdf video

Grading

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

Student presentation

Project ideas

Reading Material

Reading material related to the lesson

  • Syntax-guided synthesis
    • Alur, Bodík, Juniwal, Martin, Raghothaman, Seshia, Singh, Solar-Lezama, Torlak, Udupa: Syntax-guided synthesis. FMCAD’13
    • Gulwani: Dimensions in Program Synthesis. PPDP’10
  • Enumerative search
    • Udupa, Raghavan, Deshmukh, Mador-Haim, Martin, Alur: TRANSIT: specifying protocols with concolic snippets. PLDI’13
    • Rajeev Alur, Arjun Radhakrishna, Abhishek Udupa: Scaling Enumerative Program Synthesis via Divide and Conquer. TACAS’17
    • Phothilimthana, Thakur, Bodik, Dhurjati: Scaling Up Superoptimization. ASPLOS’16
  • Search prioritization
    • Woosuk Lee, Kihong Heo, Rajeev Alur, Mayur Naik: Accelerating Search-Based Program Synthesis usingLearned Probabilistic Models. PLDI’18
    • Barke, Peleg, Polikarpova. Just-in-Time Learning for Bottom-Up Enumerative Synthesis. OOPSLA’20.
    • Balog, Gaunt, Brockschmidt, Nowozin, Tarlow: DeepCoder: Learning to Write Programs. ICLR’17
    • Bielik, Raychev, Vechev. PHOG: Probabilistic Model for Code. ICML’16
  • Representation-based search
    • Gulwani: Automating string processing in spreadsheets using input-output examples. POPL’11
    • Polozov, Gulwani: FlashMeta: a framework for inductive program synthesis. OOPSLA’15
    • Wang, Dillig, Singh: Program synthesis using abstraction refinement. POPL’18
    • Feng, Martins, Wang, Dillig, Reps: Component-based synthesis for complex APIs. POPL’17
    • Shi, Steinhardt, Liang: FrAngel: Component-Based Synthesis with Control Structures. POPL’19
    • Willsey et al.: egg: Fast and extensible equality saturation. POPL 2021
  • Bidirectional search
    • Yoon, Lee, Yi: Inductive Program Synthesis via Iterative Forward-Backward Abstract Interpretation. PLDI 2023
    • Lee: Combining the Top-down Propagation and Bottom-up Enumeration for Inductive Program Synthesis. POPL 2021
    • Raza, Gulwani: Web Data Extraction Using Hybrid Program Synthesis: A Combination of Top-down and Bottom-up Inference. SIGMOD 2020
    • Gulwani, Korthikanti, Tiwari: Synthesizing Geometry Constructions. PLDI 2011
    • Phothilimthana, Thakur, Bodik, Dhurjati. Scaling up Superoptimization. ASPLOS 2016
  • Constraint-based search
    • Jha, Gulwani, Seshia, Tiwari: Oracle-guided component-based program synthesis. ICSE’10
    • Feng, Martins, Bastani, Dillig: Program synthesis using conflict-driven learning. PLDI’18
  • Stochastic search
    • Schkufza, Sharma, Aiken: Stochastic program optimization. CACM’16
    • Koenig, Padon, Aiken: Adaptive Restarts for Stochastic Synthesis. PLDI’21
  • Type-driven synthesis
    • Lee, Cho: Inductive Synthesis of Structurally Recursive Functional Programs from Non-Recursive Expressions. POPL’23
    • Osera, Zdancewic: Type-and-example-directed program synthesis. PLDI’15
    • Frankle, Osera, Walker, Zdancewic: Example-directed synthesis: a type-theoretic interpretation. POPL’16
    • Feser, Chaudhuri, Dillig: Synthesizing Data Structure Transformations from Input-Output Examples. PLDI 2015
    • Nadia Polikarpova, Ivan Kuraj, Armando Solar-Lezama: Program synthesis from Polymorphic Refinement Types. PLDI’16
  • Deductive synthesis
    • Reynolds, Deters, Kuncak, Tinelli, Barrett: Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV’15
    • Huang, Qiu, Shen, Wang: Reconciling enumerative and deductive program synthesis, PLDI’20
  • Applications of synthesis
    • Lee, Lee: Simplifying Mixed Boolean-Arithmetic Obfuscation by Program Synthesis and Term Rewriting. CCS’23
    • Lee, Lee, Oh, Yi: Optimizing homomorphic evaluation circuits by program synthesis and term rewriting, PLDI’20
    • Eldib, Wu, Wang: Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits, CAV’16
    • Le, Gulwani: FlashExtract: a framework for data extraction by examples. PLDI’14
    • Miltner, Gulwani, Le, Leung, Radhakrishna, Soares, Tiwari, Udupa: On the Fly Synthesis of Edit Suggestions, OOPSLA’19

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