Reading List

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?

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. RTGs) 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. $\mathcal{C}[[abort]]^{\tau}\langle \sigma, \Phi\rangle = ?$
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 $\exists c.\forall x. Q(c,x)$ 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: Neural

Xinyun Chen, Chang Liu, Dawn Song: Execution-Guided Neural Program Synthesis. ICLR'19

Questions:

What does this paper use as behavioral constraints? Structural constraint? Search strategy?
What is the key difference between their search/decoding technique and the "DP-Beam" constraints optimization in RobustFill?
Can you think of optimizations that can be applied to the search decoding in this paper's setting?
How would the execution-guidance work in case of a tree-based search decoding?
The paper deals with loop generation by unrolling them and then applies the same reasoning as for conditionals. Does this guarantee that the technique can generate arbitrarily nested loops/if statements? Illustrate your reasoning on the following example:

while frontIsClear():
  move()
  if rightIsClear():
    turnRight()
    move()
    putMarker()
    turnLeft()

Submit review here

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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Reading List

Required Reading

Week 2: EUSolver

Week 3: Euphony

Week 4: BlinkFill

Week 5: Brahma

Week 6: Sketch

Week 7: Synquid

Week 8: SuSLik

Week 9: Regae

Week 10: Neural

Recommended Reading

Week 1

Week 2

Week 3

Week 4

Week 5

Week 6

Week 7

Week 8

Week 9

Week 10

Related courses

Clone this wiki locally