CS560: Reasoning About Programs

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.

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.


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.

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.

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.
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
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

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).

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.

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.

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