CS560: Reasoning About Programs

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
Mar-26 Project Progress
Mar-28
Apr-02
Apr-04 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.”
Related courses