Schedule

Note: Schedule beyond next week is subject to change!

Day	Class Topic / Reading Assignment	Project milestone
Tue 1/09	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/11	Inductive synthesis. Syntax-guided synthesis. Enumerative search: bottom-up vs top-down. [Slides]
Tue 1/16	Search space pruning: equivalence reduction. [Slides]
Wed 1/17	EUSolver
Thu 1/18	Search space pruning: top-down constraint propagation. Condition abduction. EUSolver discussion. [Slides]
Fri 1/19		Teams
Tue 1/23	Search space prioritization. Weighted enumerative search. [Slides]
Wed 1/24	Euphony
Thu 1/25	Euphony discussion. Framework demos. Suggested project ideas.
Tue 1/30	Representation-based search: Version-Space Algebra, Finite Tree Automata. [Slides]
Wed 1/31	BlinkFill
Thu 2/1	BlinkFill discussion.
Fri 2/2		Proposal
Tue 2/6	Stochastic search, MCMC. Constraint Solving: SAT, SMT. [Slides] [Slides]
Wed 2/7	Brahma
Thu 2/8	Constraint-based search. [Slides]
	Module II: Synthesizing Complex Programs
Tue 2/13	Module I vs II. Rich specifications. Program sketching [Slides] [Slides]
Wed 2/14	Sketch
Thu 2/15	Program Sketching (cont.). [Slides]
Tue 2/20	Type Systems. Type-driven program synthesis. [Slides]
Wed 2/21	Synquid
Thu 2/22	Refinement Types. Type-driven program synthesis (cont.). [Slides]
Tue 2/27	Imperative programs. Hoare logic. Constraint-based synthesis with loop invariants. [Slides]
Wed 2/28	SuSLik
Thu 2/29	Separation logic. Deductive synthesis. [Slides]
	Module III: Advanced Topics
Tue 3/5	User interaction in synthesis. [Slides]
Wed 3/6	Regae
Thu 3/7	User interaction in synthesis (cont.)
Tue 3/12	Neural and Neuro-Symbolic synthesis. [Slides]
Wed 3/13	SatLM
Thu 3/14	Neural and Neuro-Symbolic synthesis (cont.)
Tue 3/19 3-6pm	Project Presentations.	Presentation
Fri 3/22		Report