CS590: Reasoning about Programs

Instructor Roopsha Samanta
Class Tuesday and Thursday, 4:30-5:45pm, LWSN B134
Office hours Tuesday and Thursday, 3:30-4:30pm (or by appointment), LWSN 2116L
TA Anshu Maheshwari
TA Office hours Friday, 12:00-1:00pm (or by appointment)
Prerequisites Basic knowledge of logic, set theory, algorithms and programming languages
(CS 182, CS 240, CS 381, or equivalent).
Contact the instructor if you need more information.
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 20%
Paper Presentations 15%
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 (writeup), one mid-term progress report (writeup) and the final project submission (writeup and talk). The initial project proposal and progress report will each account for 10% of the project grade. The final project presentation and writeup will account for the remaining 80% 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). No late submissions will be accepted. Contact the instructor in advance if you have a reasonable justification for any delay.

Paper Presentations
Each student will give a short lecture (~15 minutes) on a paper in class. Lectures will be evaluated on the student's understanding of the subject and communication of the subject to the rest of the class.

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

Note for auditors
You will be required to attend lectures and present a paper in class.

Note: This syllabus and schedule is tentative and may change without notice at any time. Additional readings will be provided as we go along.

Schedule
Date Topic Reading Due
Unit 1: Introduction, Logics, Core Techniques, Proof Engines
Aug-22 Course Overview  
Aug-24 Propositional and First-order Logic BM:Ch1-2
Aug-29 First-order Theories BM:Ch3
Aug-31 Axiomatic Approach to Program Verification BM:Ch4, H69
Sep-5 Axiomatic Approach to Program Verification
Sep-7 SAT Solving BM:Ch1.7, SLM08, GKSS08
Sep-12 SMT Solving BSST08, MB11
Unit 2: Sequential Programs: Verification and Analysis
Sep-14 Invariant Generation BM:Ch12Project Proposal
Sep-19 Interpolants and SAT-based Model Checking M03
Sep-21 Abstraction-Refinement JM09, BMMR01, CGJLV03
Unit 3: Concurrent Programs: Verification and Analysis
Sep-26 Introduction, Owicki-Gries Approach OG76, L77
Sep-28 Lipton's Reduction, Rely-guarantee, Partial-order Reduction EQT09,G90,D93
Oct-3 Midterm
Oct-5 Bounded Analyses, Predictive Analysis QR05,WKGG09
Oct-10 October Break  
Unit 4: Program Synthesis
Oct-12 Introduction A13,BJ13
Oct-17 Proof-based Synthesis SGF10Project Progress
Oct-19 Inductive Synthesis, PBE, Explicit Search (Version Spaces) G10
Oct-26 Structured Explicit Search (Flashfill) HG12,SG12,GHS12
Oct-24 Constraint-based Search (Sketch) STBSS06
Oct-26 Functional Synthesis (CEGIS)
Oct-31 Machine Learning for Synthesis  
Nov-2 Machine Learning for Synthesis  
Nov-7 Machine Learning for Synthesis
Nov-9 Synthesis for Concurrency VYY10,G15,C15
Nov-14 Program Repair DSS16
Nov-16 Synthesis Fest
Nov-21 Synthesis Fest
Nov-23 Thanksgiving Break  
Nov-28 Wrap-up
Nov-30 Wrap-up
Dec-5 Final Project Presentations  
Dec-7 Final Project Presentations  
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.
CES86 Edmund M. Clarke, E. Allen Emerson and A. Prasad Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic. TOPLAS, vol. 8, no. 2, 1986.
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.
MB11 Leonardo de Moura and Nikolaj Bjorner. Satisfiability Modulo Theories: Introduction and Applications. CACM, vol. 54, no. 9, 2011.
BSST08 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.
BCCZ99 Armin Biere, Alessandro Cimatti, Edmund M. Clarke and Yunshan Zhu. Symbolic Model Checking without BDDs. TACAS, 1999.
M03 Kenneth L. McMillan. Interpolation and SAT-Based Model Checking. CAV, 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.
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.
GKK05 Patrice Godefroid, Nils Klarlund and Koushik Sen. DART: Directed Automated Random Testing. PLDI, 2005.
CS03 Cristian Cadar and Koushik Sen. Symbolic Execution for Software Testing: Three Decades Later. CACM, vol. 56, no. 2, 2013.
STBSS06 Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Vijay Saraswat and Sanjit Seshia. Combinatorial Sketching for Finite Programs. ASPLOS, 2006.
SGF10 Saurabh Srivastava, Sumit Gulwani and Jeff Foster. From Program Verification to Program Synthesis. POPL, 2010.
G10 Sumit Gulwani. Automating String Processing in Spreadsheets using Input-Output Examples. POPL, 2010.
RVY14 Veselin Raychev, Martin Vechev and Eran Yahav. Code Completion with Statistical Language Models. PLDI, 2014.
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.
DSS16 Loris D'Antoni, Rishabh Singh and Roopsha Samanta. Qlose: Program Repair with Quantitative Objectives. CAV, 2016.
OG76 Susan Owicki and David Gries. Verifying Properties of Parallel Programs: An Axiomatic Approach. CACM, vol. 19, no. 5, 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.
WKGG09 Chao Wang, Sudipta Kundu, Malay Ganai and Aarti Gupta. Symbolic Predictive Analysis for Concurrent Programs. FM, 2009.
QR05 Shaz Qadeer and Jakob Rehof. Context-Bounded Model Checking of Concurrent Software. TACAS, 2005.
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.
Policies
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.”