Skip to content

Reading List

Jump to bottom
Nadia Polikarpova edited this page Feb 3, 2023 · 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?
  • What is the main technical insight of BlinkFill wrt FlashFill?
  • 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",
  • As described in the paper, the position expressions of the BlinkFill DSL only support matching a single token from Table 1, e.g. C. Could we extend the algorithm to support sequences of tokens, e.g. C ws $ to match caps followed by whitespace follows by end of string? How would this change the construction and intersection of input data graphs (use Fig 6 as an example).

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?
  • Is it possible to specify Brahma's structural constraints in the SyGuS format (as a grammar)? Is yes, show a small example. If no, explain why.
  • 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?

Submit review here

Week 6: Sketch

Armando Solar-Lezama: Program sketching. STTT’13

Questions:

  • What does Sketch use as behavioral constraints? Structural constraints? Search strategy?
  • Compare structural constraints of Sketch with those in SyGuS (i.e. CFGs) and in Brahma; which of those are more expressive?
  • Consider extending the Sketch language with a new command, abort, that makes the program fail unconditionally. What should the denotational semantics of this command be, i.e.
  • Give an example of a satisfiable synthesis constraint that violates the Bounded Observation Hypothesis, and hence cannot be efficiently solved by CEGIS. More precisely, give an example of a formula Q(c, x), where c, x are bit-vectors of size n, such that solving the constraint in the worst case would require CEGIS iterations.

Submit review here

Week 7: Synquid

Nadia Polikarpova, Ivan Kuraj, Armando Solar-Lezama: Program synthesis from Polymorphic Refinement Types. PLDI’16

Questions:

  • What does Synquid use as behavioral constraints? Structural constraint? Search strategy?
  • Find a typo in the Example is Section 3.2
  • Can Synquid's Round-Trip Type Checking discard the following incomplete terms? Explain how or why not.
    1. inc ?? :: {Int | ν = 5}, where inc :: x:Int -> {Int | ν = x + 1}
    2. duplicate ?? :: {List Int | len ν = 5}, where duplicate :: xs:List a -> {List a | len ν = 2*(len xs)}
    3. nats ?? :: List Pos, where nats :: n:Nat -> {List Nat| len ν = n}, Nat = {Int | ν >= 0}, Pos = {Int | ν > 0}
  • Compare Synquid's condition abduction mechanism to the one from EUSolver.

Submit review here

Week 8: SuSLik

Nadia Polikarpova, Ilya Sergey: Structuring the Synthesis of Heap-Manipulating Programs. POPL’19

Questions:

  • What does SuSLik use as behavioral constraints? Structural constraint? Search strategy?
  • Consider Frame rules in Fig. 1. This rule in general would not be sound if our programming language had mutable variables and assignment statements (such as x := 1). Why not? Give an example of a specification where it would be incorrect to apply the Frame rule in such an extended language.
  • Sec 5.1 introduces the invertible rule optimization. Why is the Frame rule not invertible?

Submit review here

Week 9: Regae

Tianyi Zhang, London Lowmanstone, Xinyu Wang, Elena L. Glassman: Interactive Program Synthesis by Augmented Examples. UIST'20

Questions:

  • What does Regae use as behavioral constraints? Structural constraint? Search strategy?
  • Does the semantic augmentation technique help enhance behavioral or structural constraints (or something else)? What about data augmentation?
  • Line 10 in Algorithm 1 prunes a partial regex when it is infeasible, but the paper does not focus on how infeasibility is determined. Can you come up with a condition when a partial regex can be soundly rejected? Use the regex concat(<num>,e2) as an example.
  • In the user study, they randomize the order in which the two tool variants are presented to a participant (i.e. control then treatment or treatment then control). Why is this important?

Submit review here

Week 10: TBD

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

TBD

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