Schedule

Note: Schedule beyond next week is subject to change!

Day	Class Topic / Reading Assignment	Project milestone
Tue 1/4	Course Overview: What is program synthesis? Dimensions in programs synthesis: behavioral constraints, structural constraints, search strategies. [Slides] [Synquid demo]
	Module I: Synthesizing Simple Programs
Thu 1/6	Inductive synthesis. Syntax-guided synthesis. Enumerative search: bottom-up vs top-down. [Slides]
Tue 1/11	Search space pruning: equivalence reduction. [Slides]
Wed 1/12	EUSolver
Thu 1/13	Search space pruning: top-down constraint propagation. Condition abduction. EUSolver discussion. [Slides]
Fri 1/14		Teams
Tue 1/18	Search space prioritization. Weighted enumerative search. [Slides]
Wed 1/19	Euphony
Thu 1/20	Euphony discussion. Framework demos. Suggested project ideas.
Tue 1/25	Representation-based search: Version-Space Algebra, Finite Tree Automata. [Slides]
Wed 1/26	BlinkFill
Thu 1/27	BlinkFill discussion. Stochastic search, MCMC. [Slides]
Fri 1/28		Proposal
Tue 2/1	Constraint Solving: SAT, SMT. [Slides]
Wed 2/2	Brahma
Thu 2/3	Constraint-based search. [Slides]
	Module II: Synthesizing Complex Programs
Tue 2/8	Specifications and guarantees. CEGIS. [Slides]
Wed 2/9	Sketch
Thu 2/10	Bounded constraint-based synthesis. Sketch. [Slides]
Tue 2/15	Type Systems. Type-driven program synthesis. [Slides]
Wed 2/16	Synquid
Thu 2/17	Refinement Types. Type-driven program synthesis (contd). [Slides]
Tue 2/22	Imperative programs. Hoare logic. Constraint-based synthesis with loop invariants. [Slides]
Wed 2/23	SuSLik
Thu 2/24	Separation logic. Deductive synthesis. [Slides]
	Module III: Advanced Topics
Tue 3/1	User interaction in synthesis. [Slides]
Wed 3/2	Regae
Thu 3/3	User interaction in synthesis (cont.)
Tue 3/8	Guest lecture by Alex Polozov: Neural and Neuro-Symbolic synthesis.
Wed 3/9	Neural
Thu 3/10	Guest lecture by Alex Polozov: Neural and Neuro-Symbolic synthesis (cont.)
Tue 3/15 3-6pm	Project Presentations.	Presentation
Fri 3/18		Report