Instructor	Roopsha Samanta
Class	Tuesday and Thursday, 10:30-11:45am EST (Zoom)
Office hours	Thursday, 1:30-3:00pm EST, or by appointment (Zoom)
TA	Christopher Wagner
TA Office hours	Monday, 10:00-11:30am EST, or by appointment (Zoom)
Discussion forum	Piazza (sign up here)
Prerequisites	Logic, set theory, algorithms and programming languages (CS 182, CS 240, CS 381, or equivalent). Contact the instructor if you need more information.

Note: This course is a regular graduate course and is approved for use in plans of study.

Summary

This is a graduate course on the logical foundations and algorithmic techniques used to ensure that programs do what they are supposed to do. We will focus on four key elements of automated program reasoning:

• Specification: logics to define the expected behavior of a program in a machine-readable form,
• Verification: methods to automatically check if a program meets its specification,
• Repair: methods to automatically fix a program that does not meet its specification,
• Synthesis: methods to automatically generate a correct program from a specification or an incomplete program.

While the course will primarily focus on reasoning about sequential and concurrent programs, the course will finish with a preview of the increasingly important area of reliable artifical intelligence, touching upon the latest advances in reasoning about neural networks.

The course will be an exploration of both the theory and practice of program reasoning. You will be expected to write proofs as well as tinker with SAT/SMT solvers and verification/synthesis tools.

Selected topics

• Floyd-Hoare logic
• Abstract interpretation
• Invariant generation
• Model checking
• Inductive synthesis, programming by example
• Synchronization synthesis for concurrent programs
• Reasoning about AI

Evaluation and Grading

Your final grade will be weighted as follows:

Component	Weight
Class Project	50%
Homeworks	45%
Participation	5%

Class Project for Workshop on Reasoning About Programs (WRAP) 2021

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.

We will partly simulate conference-style peer-reviewing for all papers. Each of you will serve on the Program Committee (PC) of WRAP 2021 and will review 2-3 papers by your peers. Each final paper will be reviewed by a subset of your classmates and the instructor and will be discussed in a PC meeting on the penultimate class day. While all papers will be accepted, the purpose of the PC meeting would be to rank all papers. The WRAP talks will be graded solely by the instructor.
The reviewing criteria will include originality, contribution, and presentation, and will be expanded on later in the semester.

The workshop will use "double-blind" review which means that both the reviewer and team identities are concealed from each other. To facilitate this, teams are not allowed to discuss their project specifics with other teams. Teams are allowed to discuss general aspects common to all projects with your classmates.

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.

Homeworks

There will be 4 required assignments and 1 optional assignment to test you on the theoretical aspects and common tools for program verification and synthesis. In addition, the final assignment is the set of reviews of papers assigned to you. All homeworks will be weighted equally. The optional homework will be used for extra credit.

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.

Participation

In each class, students will be evaluated for their engagement and ideas.

Note for auditors

You will be required to attend lectures.

Note: This syllabus and schedule is tentative and may be updated as we go along.

Schedule

Date	Topic	Notes	Required Reading	Due
Unit 1: Introduction, Logics, and Proof Engines
Jan-19	Course Overview	Lec. 1
Jan-21	Program Synthesis Overview, Project Ideas	Lec. 2	G10
Jan-26	Propositional Logic and Normal Forms	Lec. 3	BM:Ch1
Jan-28	SAT Solving	Lec. 4	BM:Ch1.7
Feb-02	First-order Logic	Lec. 5	BM:Ch2	HW 1
Feb-04	First-order Theories	Lec. 6	BM:Ch3
Feb-09	SMT Solving, Congruence Closure for EUF	Lec. 7	BM:Ch9
Feb-11	Temporal Logic	Lec. 8	E90	Project Proposal
Feb-16	Temporal Logic
Unit 2: Program Verification and Analysis
Feb-18	Hoare Logic I	Lec. 9	BM:Ch5,H69	HW2
Feb-23	Hoare Logic I
Feb-25	Hoare Logic II	Lec. 10
Mar-02	Invariant Generation/Abstract Interpretation	Lec. 11/12	BM:Ch12
Mar-04	Invariant Generation/Abstract Interpretation			HW 3
Mar-09	Invariant Generation/Abstract Interpretation
Mar-11	Bounded Model Checking	Lec. 13	BCCZ99
Mar-16	Model Checking	Lec. 14	CES86
Mar-18	Reading Day
Mar-23	Reading Day			HW 4
Unit 3: Program Synthesis and Repair
Mar-25	Enumerative Search (Syntax-Guided Synthesis, Inductive Synthesis)	Lec. 15	A13
Mar-30	Representation-based Search (Version Space Algebras, Finite Tree Automata}	Lec. 16	G11,WDS17	Partial Paper
Apr-01	Constraint-based Search (Sketch, CEGIS)	Lec. 17	S13
Apr-06	Constraint-based Search (Component, Proof-based Synthesis)	Lec. 18	J10,SGF10
Apr-08	Neurosymbolic Program Synthesis
Apr-13	Reading Day
Apr-15	Reading Day			HW 5 (optional)
Apr-20	Guest Lecture: Deductive Synthesis (Ben Delaware, Purdue University)
Apr-22	Guest Lecture: BluePencil (Arjun Radhakirshna, Microsoft PROSE Team)
Apr-27	Course Review			Final Paper
Apr-29	WRAP 2021			Talk Slides

Course Material

We will use one textbook and several papers in this course. Click on the textbook title for an electronic version. The papers are a mix of classic and new research papers, survey papers and handbook chapters.

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

Policies

Late policy

No late submissions will be accepted/graded unless the instructor is contacted in advance with a reasonable explanantion for the delay.

If the instructor approves late acceptance of a submission, the submission will incur a late penalty per late day (upto a maximum of 3 days). Submissions received 3 days or more after the due date will not be graded. The actual late penalty is at the instructor's discretion and may vary (based on the reason for the delay and how early the instructor was informed).

Collaboration

All submissions must be your own work. No collaboration is permitted on the project (except with your team members and instructor). No collaboration is permitted on homeworks or exams.

Academic Integrity

We will default to the Purdue University Student Code of Conduct unless stated otherwise above. You are responsible for reading the pages linked below and will be held accountable for their contents.

1. http://spaf.cerias.purdue.edu/integrity.html
2. http://spaf.cerias.purdue.edu/cpolicy.html

By taking this class, you agree to take the Purdue Honors Pledge:
“As a boilermaker pursuing academic excellence, I pledge to be honest and true in all that I do. Accountable together - we are Purdue.”

Nondiscrimination Statement

Purdue University is committed to maintaining a community which recognizes and values the inherent worth and dignity of every person; fosters tolerance, sensitivity, understanding, and mutual respect among its members; and encourages each individual to strive to reach his or her own potential. In pursuit of its goal of academic excellence, the University seeks to develop and nurture diversity. The University believes that diversity among its many members strengthens the institution, stimulates creativity, promotes the exchange of ideas, and enriches campus life. More details are available on our course Brightspace table of contents, under University Policies.

Accessibility

Purdue University strives to make learning experiences as accessible as possible. If you anticipate or experience physical or academic barriers based on disability, you are welcome to let me know so that we can discuss options. You are also encouraged to contact the Disability Resource Center at: drc@purdue.edu or by phone: 765-494-1247. More details are available on our course Brightspace under Accessibility Information.

Mental Health Statement

If you find yourself beginning to feel some stress, anxiety and/or feeling slightly overwhelmed, try WellTrack. Sign in and find information and tools at your fingertips, available to you at any time. If you need support and information about options and resources, please contact or see the Office of the Dean of Students. Call 765-494-1747. Hours of operation are Mon-Fri, 8am-5pm. If you find yourself struggling to find a healthy balance between academics, social life, stress, etc. sign up for free one-on-one virtual or in-person sessions with a Purdue Wellness Coach at RecWell. Student coaches can help you navigate through barriers and challenges toward your goals throughout the semester. Sign up is completely free and can be done on BoilerConnect. If you have any questions, please contact Purdue Wellness at evans240@purdue.edu. If you’re struggling and need mental health services: Purdue University is committed to advancing the mental health and well-being of its students. If you or someone you know is feeling overwhelmed, depressed, and/or in need of mental health support, services are available. For help, such individuals should contact Counseling and Psychological Services (CAPS) at 765-494-6995 during and after hours, on weekends and holidays, or by going to the CAPS office of the second floor of the Purdue University Student Health Center (PUSH) during business hours.

Emergency Preparation

In the event of a major campus emergency, course requirements, deadlines and grading percentages are subject to changes that may be necessitated by a revised semester calendar or other circumstances beyond the instructor’s control. Relevant changes to this course will be posted onto the course website or can be obtained by contacting the instructor or TAs via email. You are expected to read your @purdue.edu email on a frequent basis. Purdue’s Emergency Preparedness resources is located on the Brightspace shell under University Policies; this webpage includes a link to resources on COVID-19.

Modifications

This syllabus may be modified at any time with notification.

Protect Purdue Pledge

The Protect Purdue Plan, which includes the Protect Purdue Pledge, is campus policy and as such all members of the Purdue community must comply with the required health and safety guidelines. Required behaviors in this class include: staying home and contacting the Protect Purdue Health Center (496-INFO) if you feel ill or know you have been exposed to the virus, properly wearing a mask in classrooms and campus building, at all times (e.g., mask covers nose and mouth, no eating/drinking in the classroom), disinfecting desk/workspace before and after use, maintaining appropriate social distancing with peers and instructors (including when entering/exiting classrooms), refraining from moving furniture, avoiding shared use of personal items, maintaining robust hygiene (e.g., handwashing, disposal of tissues) prior to, during and after class, and following all safety directions from the instructor.

Students who are not engaging in these behaviors (e.g., wearing a mask) will be offered the opportunity to comply. If non-compliance continues, possible results include instructors asking the student to leave class and instructors dismissing the whole class. Students who do not comply with the required health behaviors are violating the University Code of Conduct and will be reported to the Dean of Students Office with sanctions ranging from educational requirements to dismissal from the university.

Any student who has substantial reason to believe that another person in a campus room (e.g., classroom) is threatening the safety of others by not complying (e.g., not properly wearing a mask) may leave the room without consequence. The student is encouraged to report the behavior to and discuss the next steps with their instructor. Students also have the option of reporting the behavior to the Office of the Student Rights and Responsibilities. See also Purdue University Bill of Student Rights

COVID-19 Policy

If you must quarantine or isolate at any point in time during the semester, please reach out to me via email so that we can communicate about how you can continue to learn remotely. Work with the Protect Purdue Health Center (PPHC) to get documentation and support, including access to an Academic Case Manager who can provide you with general guidelines/resources around communicating with your instructors, be available for academic support, and offer suggestions for how to be successful when learning remotely. Your Academic Case Manager can be reached at acmq@purdue.edu. Importantly, if you find yourself too sick to progress in the course, notify your academic case manager and notify me via email or Brightspace. We will make arrangements based on your particular situation. You can also contact the Office of the Dean of Students via email (odos@purdue.edu) or phone at 765-494-1747. Our course Brightspace includes a link to the Dean of Students under ‘Campus Resources.’

Related courses

• Rajeev Alur's course at University of Pennsylvania on program verification, analysis and synthesis
• Armando Solar-Lezamma's course at MIT on program synthesis
• Isil Dillig's course at the University of Texas at Austin on decision procedures and program verification
• Aarti Gupta's course at Princeton University on program verification and synthesis
• Nadia Polikarpova's course at University of California at San Diego on program synthesis.
• Emina Torlak's course at University of Washington on program verification and synthesis
• Martin Vechev's course at ETH on program analysis and synthesis