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.
Tue 1/25	Representation-based search: Version-Space Algebra [Slides]
Wed 1/26	BlinkFill
Thu 1/27	Finite Tree Automata, Type-Transition Nets. BlinkFill discussion. [Slides]
Fri 1/28		Proposal
Tue 2/1	Stochastic search, MCMC. Constraint Solving: SAT, SMT. [Slides] [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	TBD
Wed 3/2	TBD
Thu 3/3	TBD
Tue 3/8	TBD
Wed 3/9	TBD
Thu 3/10	TBD
Tue 3/15 3-6pm	Project Presentations.	Presentation
Fri 3/18		Report