COL 871 Special Topics in Programming Languages -- Program Synthesis

General Information


Class Timings: Mon/Wed from 18:00 hrs to 19:30 hrs Venue: Bharti 425 Instructor: Subodh Sharma (svs at cse.iitd.ac.in)


Course Info & Objectives

Program Synthesis has emerged as an effective approach to automatically create programs that meet user intent specified in the form of some specification. The technique is used successfully in diverse domains such as computer-aided education, software engineering, software verification etc. In this course we will discuss modern synthesis approaches by discussing foundational as well as recent research advances in this area. Topics covered in this course will include enumerative syntax-guided synthesis, counterexample-guided synthesis, stochastic synthesis and machine-learning based synthesis.

Academic Integrity:

Plagiarism is viewed very seriously. Any case of copying (or allowing to copy) of written text or code would immediately be awarded 0 in the assignment/exam and a grade drop. Depending on the nature of plagiarism, the student could also be refered to the disciplanary committee with a fail grade. All written/programming tasks are to performed on your own, other than when group-work is explicitly specified.

Lecture Material

Sr. No. Topic Supplementary Reading
1 Course modalities; Introduction
2, 3 Denali: A Goal-directed Superoptimizer
  • Stochastic Superoptimization (ASPLOS'13)
  • Equality saturation: a new approach to optimization (POPL'09)
  • Automatic generation of peephole superoptimizers (ASPLOS'06)
  • Synthesis of loop-free programs (PLDI'11)
  • Scaling up Superoptimization (ASPLOS'16)
4-6 Program Synthesis by Sketching
  • Sketching Stencils (PLDI'07)
  • Sketching Concurrent Data strucutures (PLDI'08)
  • Optimizing Synthesis with Metasketches (POPL'16)
7-8 Syntax Guided Synthesis & Search-based Program Synthesis
  • Synthesis Through Unification (CAV'15)
9-11 Spreadsheet Data Manipulation Using Examples
  • Synthesizing Data Structure Transformations from Input-Output Examples (PLDI'15)
  • Test-driven synthesis (PLDI'14)
  • Learning Syntactic Program Transformations from Examples (ICSE'17)
  • Scaling Enumerative Program Synthesis via Divide and Conquer (TACAS'17)
  • Synthesizing highly expressive SQL queries from input-output examples (PLDI'17)
12-13 From Program Verification to Program Synthesis
  • ICE: A robust Framework for Learning Invariants (CAV'14)
  • Type-and-example-directed Program Synthesis (PLDI'15)
  • Program Synthesis using Abstraction Refinement (POPL'18)
  • Program Synthesis using Conflict-Driven Learning (PLDI'18)
14-16 Stochastic Program Optimization
  • Data-driven Equivalence Checking (OOPSLA'13)
  • Finding deep compiler bugs via guided stochastic program mutation (OOPSlA'15)
  • Guided, stochastic model-based GUI testing of Android apps (FSE'17)
  • Sampling for Bayesian Program Learning (NIPS'16)
  • Code Completion with Statistical Language Models (PLDI'14)
17 Course Project Discussions
18-22 Neural Program Learning under Noisy I/O (ICML'17)
  • Nueral-guided Deductive Search for Realtime Program Synthesis from Examples (ICLR'18)
  • Learning Programs from Noisy Data (POPL'16)
  • Neuro-Symbolic Program Synthesis (ArXiv'16)
  • Learn & Fuzz: Machine learning for input fuzzing (ASE'17)
23-28 Course Project Presentations