Skip to content

Reading List

Jump to bottom
Nadia Polikarpova edited this page Feb 2, 2024 · 118 revisions

Note: the list of required papers beyond next week is subject to change!

Required Reading

Week 2: EUSolver

Rajeev Alur, Arjun Radhakrishna, Abhishek Udupa: Scaling Enumerative Program Synthesis via Divide and Conquer. TACAS'17

Questions:

  • What does EUSolver use as behavioral constraints? Structural constraint? Search strategy?
  • What are the main two pruning/decomposition techniques EUSolver uses to speed up the search? What enables these techniques?
  • What would a naive alternative to decision tree learning be for synthesizing branch conditions? What are the disadvantages of this alternative?

Submit review here

Week 3: Euphony

Woosuk Lee, Kihong Heo, Rajeev Alur, Mayur Naik: Accelerating Search-Based Program Synthesis usingLearned Probabilistic Models. PLDI'18

Questions:

  • What does Euphony use as behavioral constraints? Structural constraint? Search strategy? How are they different from EUSolver?

  • Consider Fig 2b, where the synthesizer is unrolling the sentential form Rep(x,"-",S). When the search is guided by a PHOG, it considers the weighted productions shown in Fig 2a (top). What would these productions look like if we replaced the PHOG with a PCFG? With 3-grams? Do you think these other probabilistic models would work as well as a PHOG?

  • Consider Example 3.2. Explain in English the intuitive meaning of h(S) = 0.1 and why it is the case.

  • Consider Theorem 3.7. Give an example of sentential forms n_i, n_j and set of points pts such that n_i and n_j are equivalent on pts but not weakly equivalent.

Submit review here

Week 4: BlinkFill

Rishabh Singh: BlinkFill: Semisupervised Programming By Example for Syntactic String Transformations. VLDB'16

Questions:

  • What does BlinkFill use as behavioral constraints? Structural constraints? Search strategy?
  • Write a program in the BlinkFill DSL (L_s) that extracts conference acronyms and years; the program should satisfy the following examples:
    • "Programming Language Design and Implementation (PLDI), 2019, Phoenix AZ" -> "PLDI 2019"
    • "Principles of Programming Languages (POPL), 2020, New Orleans LA" -> "POPL 2020",
  • How does BlinkFill use the IDG to help synthesis? (Is it used for pruning or prioritization? Does it make things faster or does it make the results better?)
  • Why can BlinkFill "afford" to use constant tokens in its regexes and FlashFill cannot?

Submit review here

Week 5: Brahma

Sumit Gulwani, Susmit Jha, Ashish Tiwari, Ramarathnam Venkatesan: Synthesis of loop-free programs. PLDI'11

Questions:

  • What does Brahma use as behavioral constraints? Structural constraints? Search strategy?
  • Brahma's SMT encoding has an integer variable per component, which denotes the line where the component is to be placed. An alternative encoding is to have an integer variable per line, which denotes which component is to be placed into that line. Compare these two alternatives in terms of the size of the search space and the amount of domain knowledge they require. When should I prefer one over the other?
  • Consider the following modification of Brahma's synthesis problem: you are given N components, but your program is only allowed to use any K of them (for a fixed K <= N). How would you modify the SMT encoding in section 5 to enforce this restriction?
  • Does the CEGIS loop in Fig 2 still work if the component specifications in $\phi_{lib}$ are imprecise? E.g. you can assume that one of the components has a trivial specification true.

Submit review here

Recommended Reading

Week 1

Gulwani: Dimensions in Program Synthesis. PPDP'10

Alur, Bodík, Juniwal, Martin, Raghothaman, Seshia, Singh, Solar-Lezama, Torlak, Udupa: Syntax-guided synthesis. FMCAD'13

Week 2

Udupa, Raghavan, Deshmukh, Mador-Haim, Martin, Alur: TRANSIT: specifying protocols with concolic snippets. PLDI'13

Albarghouthi, Gulwani, Kincaid: Recursive Program Synthesis. CAV'13

Barke, Peleg, Polikarpova. Just-in-Time Learning for Bottom-Up Enumerative Synthesis. OOPSLA'20.

Phothilimthana, Thakur, Bodik, Dhurjati: Scaling Up Superoptimization. ASPLOS’16

Lee: Combining the top-down propagation and bottom-up enumeration for inductive program synthesis POPL'21

Smith, Albarghouthi Program Synthesis with Equivalence Reduction. VMCAI'19

Feser, Chaudhuri, Dillig: Synthesizing Data Structure Transformations from Input-Output Examples. PLDI 2015

Week 3

Balog, Gaunt, Brockschmidt, Nowozin, Tarlow: DeepCoder: Learning to Write Programs. ICLR'17

Bielik, Raychev, Vechev. PHOG: Probabilistic Model for Code. ICML’16

Barke, Peleg, Polikarpova. Just-in-Time Learning for Bottom-Up Enumerative Synthesis . OOPSLA'20.

Shi, Bieber, Singh TF-Coder: Program Synthesis for Tensor Manipulations . TOPLAS'22

Week 4

Gulwani: Automating string processing in spreadsheets using input-output examples. POPL'11

Le, Gulwani: FlashExtract: a framework for data extraction by examples. PLDI'14

Polozov, Gulwani: FlashMeta: a framework for inductive program synthesis. OOPSLA’15

Wang, Dillig, Singh: Program synthesis using abstraction refinement. POPL'18

Koppel, Guo, de Vries, Solar-Lezama, Polikarpova: Searching Entangled Program Spaces. ICFP'22

Willsey, Nandi, Wang, Flatt, Tatlock, Panchekha: egg: Fast and Extensible Equality Saturation. POPL’21

Week 5

Schkufza, Sharma, Aiken: Stochastic program optimization. CACM’16

Shi, Steinhardt, Liang: FrAngel: Component-Based Synthesis with Control Structures. POPL'19

Nieuwenhuis, Oliveras, Tinelli: Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T). JACM'06

Jha, Gulwani, Seshia, Tiwari: Oracle-guided component-based program synthesis. ICSE’10

Feng, Martins, Bastani, Dillig: Program synthesis using conflict-driven learning. PLDI'18

Week 6

Torlak, Bodik: A Lightweight Symbolic Virtual Machinefor Solver-Aided Host Languages. PLDI'14

Week 7

Osera, Zdancewic: Type-and-example-directed program synthesis. PLDI'15

Frankle, Osera, Walker, Zdancewic: Example-directed synthesis: a type-theoretic interpretation. POPL'16

Düdder, Martens, Rehof: Staged Composition Synthesis. ESOP'14

Scherer, Rémy: Which simple types have a unique inhabitant?. ICFP'15

Knoth, Wang, Polikarpova, Hoffman: Resource-Guided Program Synthesis. PLDI'19

Week 8

Srivastava, Gulwani, Foster: From program verification to program synthesis. POPL'10

Qiu, Solar-Lezama: Natural Synthesis of Provably-Correct Data-Structure Manipulations. OOPSLA'17

Kneuss, Kuraj, Kuncak, Suter: Synthesis modulo recursive functions. OOPSLA’13

Manna, Waldinger: Synthesis: Dreams → Programs. TSE'79

Manna, Waldinger: A Deductive Approach to Program Synthesis. TOPLAS'80

Reynolds, Deters, Kuncak, Tinelli, Barrett: Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV'15

Week 9

Sarah E. Chasins, Maria Mueller, Rastislav Bodík: Rousillon: Scraping Distributed Hierarchical Web Data UIST'18

Ian Drosos, Titus Barik, Philip J. Guo, Robert DeLine, Sumit Gulwani: Wrex: A Unified Programming-by-Example Interaction for Synthesizing Readable Code for Data Scientists. CHI'20

Kasra Ferdowsifard, Allen Ordookhanians, Hila Peleg, Sorin Lerner, Nadia Polikarpova: Small-Step Live Programming by Example. UIST'20

Michael B. James, Zheng Guo, Ziteng Wang, Shivani Doshi, Hila Peleg, Ranjit Jhala, Nadia Polikarpova: Digging for Fold: Synthesis-Aided API Discovery for Haskell. OOPSLA'20.

Hila Peleg, Roi Gabay, Shachar Itzhaky, Eran Yahav: Programming with a Read-Eval-Synth Loop. OOPSLA 2020

Week 10

Jacob Devlin, Jonathan Uesato, Surya Bhupatiraju, Rishabh Singh, Abdel-rahman Mohamed, Pushmeet Kohli. RobustFill: Neural Program Learning under Noisy I/O

Ashwin K. Vijayakumar, Dhruv Batra, Abhishek Mohta, Prateek Jain, Oleksandr Polozov, Sumit Gulwani. Neural-Guided Deductive Search for Real-Time Program Synthesis from Examples

Mark Chen et al. Evaluating Large Language Models Trained on Code

Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie Cai, Michael Terry, Quoc Le, Charles Sutton. Program Synthesis with Large Language Models

Related courses

  • Roopsha Samanta's course at Purdue on program verification and synthesis
  • Isil Dillig's course at the University of Texas at Austin on decision procedures and program verification
  • Armando Solar-Lezamma's course at MIT on program synthesis
  • Emina Torlak's course at University of Washington on program verification and synthesis
  • Rajeev Alur's course at University of Pennsylvania on program verification, analysis and synthesis
  • Aarti Gupta's course at Princeton University on program verification and synthesis
Clone this wiki locally