Instructor | Roopsha Samanta |
Class | Tuesday and Thursday, 10:30-11:45am EST (WALC 2127) |
Office hours | TBD |
TA | Yongwei Yuan |
TA Office hours | TBD |
Discussion forum | TBD |
Prerequisites | Logic, set theory, algorithms and programming languages (CS 182, CS 240, CS 381, or equivalent). Contact the instructor if you need more information. |
Component | Weight |
---|---|
Class Project | 45% |
Midterm | 20% |
Homeworks | 30% |
Participation | 5% |
You will work (in teams of 2 or 3) to produce a research paper and present an accompanying talk on program synthesis at WRAP 2021. The project description will be provided in Lecture 2. Each team will specialize the project to their preferred application domain.
There are four submissions for the class project: the initial project proposal identifying the application domain, a partial version of the paper, the final paper, and the final talk.
The initial project proposal and partial paper will be submitted primarily for feedback from the instructor and will not be graded. The final paper and talk will account for 100% of the project grade. The evaluation criteria will include originality, contribution, and presentation.
All submissions should be uploaded to Brightspace by 6:00pm on their due days unless otherwise specified (see the schedule).
Contact the instructor in advance if you have a reasonable justification for any delay.
There will be 5 required assignments to test you on the theoretical aspects and common tools for program verification and synthesis.
All homeworks will be weighted equally.
Homeworks should be uploaded to Brightspace (unless otherwise stated) by 6:00pm on their due days unless otherwise specified (see the schedule). Contact the instructor in advance if you have a reasonable justification for any delay.
Date | Topic | Notes | Required Reading | Due |
---|---|---|---|---|
Unit 1: Foundations: Logics and Proof Engines | ||||
Aug-24 | Course Overview | Lec. 1 | ||
Aug-26 | Propositional Logic and Normal Forms | Lec. 2 | BM:Ch1 | |
Aug-31 | SAT Solving | Lec. 3 | BM:Ch1.7 | |
Sep-02 | First-order Logic | Lec. 4 | BM:Ch2 | HW 1 |
Sep-07 | First-order Theories | Lec. 5 | BM:Ch3 | |
Sep-09 | SMT Solving, Congruence Closure for EUF | Lec. 6 | BM:Ch9 | |
Sep-14 | Hoare Logic I | Lec. 7 | BM:Ch5,H69 | |
Sep-16 | Hoare Logic II | Lec. 8 | HW 2 | |
Unit 2: Program Synthesis | ||||
Sep-21 | Program Synthesis Overview, Project Ideas | Lec. 9 | G10 | |
Sep-23 | Enumerative Search (Syntax-Guided Synthesis, Inductive Synthesis) | Lec. 10 | A13 | |
Sep-28 | Representation-based Search (Version Space Algebras, Finite Tree Automata} | Lec. 11 | G11,WDS17 | Project Proposal |
Sep-30 | Constraint-based Search (Sketch, CEGIS) | Lec. 12 | S13 | HW 3 |
Oct-05 | Constraint-based Search (Component, Proof-based Synthesis) | Lec. 13 | J10,SGF10 | |
Oct-07 | Guest Lecture: BluePencil (Arjun Radhakirshna, Microsoft PROSE Team) | |||
Oct-12 | October Break | |||
Oct-14 | Guest Lecture: Deductive Synthesis (Ben Delaware, Purdue University) | HW 4 | ||
Oct-19 | Midterm | |||
Oct-21 | Neuro-Symbolic Program Synthesis | |||
Unit 3: Program Verification and Analysis | ||||
Oct-26 | Invariant Generation/Abstract Interpretation | Lec. 14 | BM:Ch12 | |
Oct-28 | Invariant Generation/Abstract Interpretation | |||
Nov-02 | Temporal Logic | Lec. 15 | E90 | Partial Paper |
Nov-04 | Model Checking | Lec. 16 | CES86 | |
Nov-09 | Bounded Model Checking | Lec. 17 | BCCZ99 | |
Nov-11 | Predicate Abstraction | HW 5 | ||
Dec-02 | Course Review | |||
Dec-07 | WRAP | |||
Dec-09 | WRAP | Talk Slides, Final paper |
Textbook | ||
BM | Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. 2007. | |
Required/Recommended Papers by Lecture | ||
Lecture 2 | ||
G10 | Sumit Gulwani. Dimensions in Program Synthesis. PPDP. 2010. | |
BJ13 | Rastislav Bodik and Barbara Jobstmann: Algorithmic Program Synthesis: Introduction. JSTT. 2013. | |
GPS17 | Sumit Gulwani, Alex Polozov, and Rishabh Singh. Program Synthesis. Foundations and Trends in Programming Languages. 2010. | |
Lecture 4 | ||
G08 | Carla P. Gomes, Henry Kautz, Ashish Sabharwal, and Bart Selman. Satisfiability Solvers. Handbook of Knowledge Representation: Chapter 2. 2008. | |
SLM08 | Joao Marques-Silva, Ines Lynce and Sharad Malik. Conflict-Driven Clause Learning SAT Solvers. Handbook of Satisfiability: Chapter 4. 2008. | |
Lecture 7 | ||
B08 | Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability Modulo Theories. Handbook of Satisfiability: Chapter 12. 2008. | |
LM08 | Chu Min Li and Felip Manyà. MaxSAT, Hard and Soft Constraints. Handbook of Satisfiability: Chapter 19. 2008. | |
MB11 | Leonardo de Moura and Nikolaj Bjorner. Satisfiability Modulo Theories: Introduction and Applications. CACM. 2011. | |
Lecture 8 | ||
E90 | E. Allen Emerson. Temporal and Modal Logic. Handbook of Theoretical Computer Science: Formal Models and Semantics. 1990. | |
PP18 | Nir Piterman and Amir Pnueli. Temporal Logic and Fair Discrete Systems. Handbook of Model Checking. 2018. | |
Lecture 9 | ||
H69 | C. A. R. Hoare. An Axiomatic Basis for Computer Programming. CACM. 1969. | |
Lecture 13 | ||
B99 | Armin Biere, Alessandro Cimatti, Edmund M. Clarke and Yunshan Zhu. Symbolic Model Checking without BDDs. TACAS. 1999. | |
CKY03 | Edmund M. Clarke, Danial Kroening and Karen Yorav. Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking. DAC. 2003. | |
M03 | Kenneth L. McMillan. Interpolation and SAT-Based Model Checking. CAV. 2003. | |
Lecture 14 | ||
CE81 | Edmund M. Clarke and E. Allen Emerson. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. Workshop on Logics of Programs. 1981. | |
CES86 | Edmund M. Clarke, E. Allen Emerson and A. Prasad Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic. TOPLAS. 1986. | |
VW86 | Moshe Y. Vardi and Pierre Wolper. An Automata-theoretic Approach to Automatic Program Verification. LICS. 1986. | |
H18 | Gerard J. Holzmann. Explicit-State Model Checking. Handbook of Model Checking. 2018. | |
Lecture 15 | ||
A13 | Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak and Abhishek Udupa: Syntax-Guided Synthesis. FMCAD, 2013. | |
U13 | Abhishek Udupa, Arun Raghavan, Jyotirmoy V. Deshmukh, Sela Mador-Haim, Milo M.K. Martin, and Rajeev Alur. TRANSIT: Specifying Protocols with Concolic Snippets. PLDI. 2013 | |
ARU17 | Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa. Scaling Enumerative Program Synthesis via Divide and Conquer. TACAS. 2017 | |
Lecture 16 | ||
G11 | Sumit Gulwani. Automating String Processing in Spreadsheets using Input-Output Examples. POPL. 2011. | |
HG12 | William Harris and Sumit Gulwani. Spreadsheet Table Transformations from Examples. PLDI. 2012. | |
SG12 | Rishabh Singh and Sumit Gulwani. Learning Semantic String Transformations from Examples. VLDB. 2012. | |
GHS12 | Sumit Gulwani, William Harris and Rishabh Singh. Spreadsheet Data Manipulation using Examples. CACM. 2012. | |
LG14 | Vu Le and Sumit Gulwani. FlashExtract: A Framework for Data Extraction by Examples. PLDI. 2014. | |
PG15 | Alex Polozov and Sumit Gulwani. FlashExtract: FlashMeta: A Framework for Inductive Program Synthesis. OOPSLA. 2015. | |
WDS17 | Xinyu Wang, Isil Dillig, and Rishabh Singh Synthesis of Data Completion Scripts using Finite Tree Automata OOPSLA. 2017 | |
WDS18 | Xinyu Wang, Isil Dillig, and Rishabh Singh. Program Synthesis using Abstraction Refinement. POPL. 2018 | |
Lecture 17 | ||
S06 | Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Vijay Saraswat and Sanjit Seshia. Combinatorial Sketching for Finite Programs. ASPLOS. 2006. | |
S13 | Armando Solar-Lezama. Program Sketching. STTT. 2013. | |
Lecture 18 | ||
J10 | Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, Ashish Tiwari Oracle-Guided Component-Based Program Synthesis ICSE . 2010 | |
GJ11 | Sumit Gulwani, Susmit Jha, Ashish Tiwari and Ramarathnam Venkatesan Synthesis of Loop-free Programs. PLDI. 2011 | |
SGF10 | Saurabh Srivastava, Sumit Gulwani and Jeff Foster. From Program Verification to Program Synthesis. POPL. 2010. | |
Inductive Synthesis Papers (Project) | ||
Data Wrangling (see also, Papers for Lec. 20) | ||
SG12 | Rishabh Singh, Sumit Gulwani Synthesizing Number Transformations from Input-Output Examples. CAV. 2012 | |
PGGP14 | Daniel Perelman, Sumit Gulwani, Dan Grossman and Peter Provost Test-Driven Synthesis. PLDI. 2014 | |
SG15 | Rishabh Singh, Sumit Gulwani Predicting a Correct Program in Programming by Example. CAV. 2015 | |
BGHZ15 | Daniel W. Barowy, Sumit Gulwani, Ted Hart and Benjamin Zorn FlashRelate: Extracting Relational Data from Semi-Structured Spreadsheets Using Examples. PLDI. 2015 | |
SG16 | Rishabh Singh, Sumit Gulwani Transforming Spreadsheet Data Types using Examples. PLDI. 2016 | |
S16 | Rishabh Singh Blinkfill: Semi-supervised Programming by Example for Syntactic String Transformations VLDB. 2016 | |
D17 | Jacob Devlin, Jonathan Uesato, Surya Bhupatiraju, Rishabh Singh, Abdelrahman Mohamed, Pushmeet Kohli RobustFill: Neural Program Learning under Noisy I/O. ICML. 2017 | |
F17 | Yu Feng, Ruben Martins, Jacon Van Geffen, Isil Dillig, and Swarat Chaudhuri Component-Based Synthesis of Table Consolidation and Transformation Tasks from Examples. PLDI. 2017 | |
SQL/Datalog Queries | ||
ZS13 | Sai Zhang, Yuyin Sun Automatically Synthesizing SQL Queries from Input-Output Examples ASE. 2013 | |
WCB17 | Chenglong Wang, Alvin Cheung, Rastislav Bodik Synthesizing Highly Expressive SQL Queries from Input-Output Examples PLDI. 2017 | |
WCB17 | Xujie Sie, Woosuk Lee, Richard Zhang, Aws Albarghouthi, Paraschos Koutris, and Mayur H Naik. Bernhard Scholz. Syntax-Guided Synthesis of Datalog Programs. FSE. 2018 | |
RMZNS19 | Mukund Raghothaman, Jonathan Mendelson, David Zhao, Mayur Naik, and Bernhard Scholz. Provenance-Guided Synthesis of Datalog Programs. POPL. 2019 | |
Parsers | ||
LSL15 | Alan Leung, John Sarracino, Sorin Lerner Interactive Parser Synthesis by Example PLDI. 2015 | |
Recursive Programs | ||
AGK17 | Aws Albargouthi, Sumit Gulwani, and Zachary Kincaid. Recursive Program Synthesis. CAV. 2013 | |
FCD15 | John K. Feser, Swarat Chaudhuri, Isil Dillig Synthesizing Data Structure Transformations from Input-Output Examples. PLDI. 2015 | |
OZ15 | Peter-Michael Osera and Steve Zdancewic. Type-and-Example-Directed Program Synthesis. PLDI. 2015 | |
YKDC16 | Navid Yaghmazadeh, Christian Klinger, Isil Dillig, Swarat Chaudhuri Synthesizing Transformations on Hierarchically Structured Data. PLDI. 2016 | |
Miscellaneous Domains | ||
M05 | David Mandelin, Lin Xu, Rastislav Bodik, Doug Kimelman Jungloid Mining: Helping to Navigate the API Jungle PLDI, 2005 | |
SA16 | Calvin Smith, Aws Albarghouthi MapReduce Program Synthesis. PLDI. 2016 | |
F17 | Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, Thomas W. Reps Component-Based Synthesis for Complex APIs. POPL 2017 | |
ASV17 | Loris D’Antoni, Rishabh Singh, Michael Vaughn NoFAQ: Synthesizing Command Repairs from Examples. FSE. 2017 | |
IS18 | Jeevana P. Inala and Rishabh Singh WebRelate: Integrating Web Data with Spreadsheets using Examples. POPL. 2018 |