Instructor	Roopsha Samanta
Class	Tuesday and Thursday, 6:00-7:15pm, LWSN B134
Office hours	Tuesday, 1:30-3:00pm (or by appointment), LWSN 2116L
TA	Shengwei An
TA Office hours	Friday, 9:00-10:00am (or by appointment), HAAS G50
Online 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.

We will consider sequential and concurrent programs and, if time permits, probabilistic programs.

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
• SAT-based model checking, interpolants
• Invariant generation
• Assume-guarantee reasoning
• Inductive synthesis, programming by example
• Machine-learning based program synthesis
• Synchronization synthesis for concurrent programs

Evaluation and Grading

Your final grade will be weighted as follows:

Component	Weight
Class Project	40%
Midterm	20%
Homeworks	35%
Participation	5%

Class Project

You will work (alone or in teams of 2) on an open-ended course project. In the project, you may conduct original research in the broad areas of automated program verification and synthesis, or comprehensively survey a topic not covered in the course. I can help you finalize a project topic.

There are three milestones for the class project - the initial project proposal, one mid-term progress report and the final project submission (presentation and project report). The initial project proposal and progress report will be short writeups submitted primarily for feedback from the instructor. The final project presentation and writeup will account for 100% of the project grade.

Projects will be evaluated for their originality, contribution and presentation.

All writeups should be uploaded to Piazza by midnight on their due days (see the schedule). Contact the instructor in advance if you have a reasonable justification for any delay.

Homeworks

There will be five homeworks, of which four will be theoretical and programming assignments based on the course material and one will involve writing up a publicly-available paper summary. All homeworks will be weighted equally.

All homeworks should be uploaded to Piazza (unless otherwise stated) by 5:30pm on their due days (see the schedule).

Participation

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

Note for auditors

You will be required to attend lectures and do the paper summary homework.

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

Schedule

Date	Topic	Reading	Due
Unit 1: Introduction, Logics, Core Techniques, Proof Engines
Jan-08	Course Overview
Jan-10	Propositional and First-order Logic	BM:Ch1-2
Jan-15	First-order Logic	BM:Ch2
Jan-17	First-order Theories	BM:Ch3
Jan-22	SAT Solving	BM:Ch1.7, GKSS08, SLM08
Jan-24	SMT Solving, Congruence Closure for EUF	BSST08, MB11, BM:Ch9	HW 1
Jan-29	Hoare Logic I	BM:Ch5, H69
Jan-31	Snow Day
Unit 2: Program Verification and Analysis
Feb-05	Hoare Logic II
Feb-07	Invariant Generation/Abstract Interpretation	BM:Ch12	HW 2
Feb-12	Invariant Generation/Abstract Interpretation
Feb-14	Abstraction-Refinement/Predicate Abstraction	JM09, BMMR01, HJMS02, CGJLV03	Project Proposal
Feb-19	Bounded Model Checking	BCCZ99, CKY03
Feb-21	Model Checking and Temporal Logic	CE81	HW 3
Feb-26	Class cancelled
Feb-28	Midterm
Mar-05	Model Checking and Temporal Logic, Odds and Ends
Mar-07	Concurrent Program Verification: Owicki-Gries Approach	OG76, L77
Mar-12	Spring Break
Mar-14	Spring Break
Mar-19	Concurrent Program Analysis: Bounded Analyses, Predictive Analysis	QR05,WKGG09	HW 4
Unit 3: Program Synthesis and Repair
Mar-21	Introduction	G10,A13,BJ13
Mar-26	Inductive Synthesis, Explicit Search		Project Progress
Mar-28	Search using Version Space Algebras (FlashFill)	G11,HG12,SG12,GHS12
Apr-02	Constraint-based Search (Sketch, CEGIS)	STBSS06
Apr-04	Constraint-based Search (Component, Proof-based Synthesis)	GJTV11,JGST10,SGF10	HW 5
Apr-09
Apr-11	No class. Attend Nadia Polikarpova's PurPL talk on Apr-12
Apr-16	Synthesis for Concurrency	VYY10,G15,C15
Apr-18	Program Repair	DSS16
Apr-23	Final Project Presentations
Apr-25	Final Project Presentations
Apr-30			Project Report

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.
Papers
H69	C. A. R. Hoare. An Axiomatic Basis for Computer Programming. CACM, vol. 12., no. 10, 1969.
GKSS08	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.
BSST08	Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability Modulo Theories. Handbook of Satisfiability, Chapter 12, 2008.
MB11	Leonardo de Moura and Nikolaj Bjorner. Satisfiability Modulo Theories: Introduction and Applications. CACM, vol. 54, no. 9, 2011.
LM08	Chu Min Li and Felip Manyà. MaxSAT, Hard and Soft Constraints. Handbook of Satisfiability, Chapter 19, 2008.
BCCZ99	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.
JM09	Ranjit Jhala and Rupak Majumdar. Software Model Checking. ACM Computing Surveys, vol. 41, no. 4, 2009.
BMMR01	Thomas Ball, Rupak Majumdar, Todd Millstein and Sriram K. Rajamani. Automatic Predicate Abstraction of C Programs. PLDI, 2001.
HJMS02	Tom Henzinger, Ranjit Jhala, Rupak Majumdar and Grégoire Sutre. Lazy Abstraction of C Programs. POPL, 2002.
CGJLV03	Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu and Helmut Veith. Counterexample-guided Abstraction Refinement for Symbolic Model Checking. JACM, vol. 50, no. 5, 2003.
OG76	Susan Owicki and David Gries. An Axiomatic Proof Technique for Parallel Programs I. Acta Informatica, vol. 6, no. 4, 1976.
L77	Leslie Lamport. Proving the Correctness of Multiprocess Programs. Trans. on Software Engineering, vol. 3, no. 2, 1977.
EQT09	Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran. A Calculus of Atomic Actions. POPL, 2009.
G90	Patrice Godefroid. Using Partial Orders to Improve Automatic Verification Methods. CAV, 1990.
D93	Doron Peled. All from One, One for All: On Model Checking Using Representatives. CAV, 1993.
QR05	Shaz Qadeer and Jakob Rehof. Context-Bounded Model Checking of Concurrent Software. TACAS, 2005.
WKGG09	Chao Wang, Sudipta Kundu, Malay Ganai and Aarti Gupta. Symbolic Predictive Analysis for Concurrent Programs. FM, 2009.
G10	Sumit Gulwani. Dimensions in Program Synthesis. PPDP, 2010.
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.
BJ13	Rastislav Bodik and Barbara Jobstmann: Algorithmic Program Synthesis: Introduction. JSTT, 2013.
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.
STBSS06	Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Vijay Saraswat and Sanjit Seshia. Combinatorial Sketching for Finite Programs. ASPLOS, 2006.
GJTV11	Sumit Gulwani, Susmit Jha, Ashish Tiwari and Ramarathnam Venkatesan Synthesis of Loop-free Programs. PLDI 2011
JGST10	Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, Ashish Tiwari Oracle-Guided Component-Based Program Synthesis ICSE, 2010
SGF10	Saurabh Srivastava, Sumit Gulwani and Jeff Foster. From Program Verification to Program Synthesis. POPL, 2010.
RVY14	Veselin Raychev, Martin Vechev and Andreas Krause. Predicting Program Properties from “Big Code”. PPL, 2015.
P17	Emilio Parisotto, Abdelrahman Mohamed, Rishabh Singh, Lihong Li, Denny Zhou, Pushmeet Kohli Neuro-Symbolic Program Synthesis. ICLR 2017
VYY10	Martin Vechev, Eran Yahav and Greta Yorsh. Abstraction-guided Synthesis of Synchronization. POPL, 2010.
G15	Ashutosh Gupta, Thomas A. Henzinger, Arjun Radhakrishna, Roopsha Samanta and Thorsten Tarrach Succinct Representation of Concurrent Trace Sets. POPL, 2015.
C15	Pavol Cerny, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta and Thorsten Tarrach. From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis. CAV, 2015.
DSS16	Loris D'Antoni, Rishabh Singh and Roopsha Samanta. Qlose: Program Repair with Quantitative Objectives. CAV, 2016.

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 project write-ups (except with your project partner if you have one). No collaboration is permitted on homeworks or exams.

We will default to Purdue's academic policies 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.”