CS59000: Computer-Aided Program Reasoning

Instructor Roopsha Samanta
Class Tuesday and Thursday, 3:00-4:15pm, Recitation Building 103
Office hours Tuesday and Thursday, 4:30-5:30pm (or by appointment), LWSN 2116L
Online forum Piazza (sign up here)
Prerequisites Basic knowledge of logic, algorithms and programming languages.
Contact the instructor if you need more information.
Summary
As software increasingly runs our lives, can we effectively reason about and ensure software reliability? In this seminar, we will focus on logical foundations and algorithmic techniques for guaranteeing that programs meet certain properties. At the end of the seminar, you will have an insight into the following questions:
  • How can one specify program correctness?
  • How can one check if a program is correct?
  • How can one automatically synthesize a correct program or program component?

Format
The seminar explores a series of topics in automated program reasoning through readings of relevant book chapters and papers. Some of the topics will be presented as lectures by the instructor. Most topics, though, will be tackled through student-led, active learning sessions. In each such class, the lead student will present a 30-45 minutes summary of the assigned paper(s), followed by a classroom discussion. The paper summary may be delivered lecture-style on a whiteboard or using slides. Student presenters should meet the instructor about 1 week before their lecture to discuss the outline.

To prepare for the discussion, each of you must read the assigned paper(s) and submit brief reviews prior to class. The review must summarize the paper and highlight the contributions. In class, each of you will articulate your thoughts about the merits, drawbacks and possible extensions of the paper/topic.

You will also 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 seminar. I can help you finalize a project topic.

Evaluation and Grading
Your final grade will be weighted as follows:
Component Weight
Class Project 40%
Paper Presentations 30%
Paper Reviews 15%
Participation 15%
Class Project
There are four milestones for the class project - the initial project proposal, two mid-term progress reports and the final project submission. Each milestone involves a talk and a writeup. The initial project proposal and progress reports will each account for 10% of the project grade. The final project presentation and writeup will account for the remaining 70% of the project grade.

Projects will be evaluated for their content and presentation. Extra credit will be given for originality of thought and approach.

The writeups for the proposal and progress reports should be uploaded to Piazza by noon on their allotted days in the schedule (see below). No late submissions will be accepted. The final project write is due by midnight on Dec 8, 2016. There will be a late penalty of 10% of the final project grade per day. Contact the instructor if you have a reasonable justification for the delay.

Paper Presentations
Each student will pick two dates from the schedule and present a lecture on the topic for each date. The lectures will be evaluated on the student's understanding and presentation of the subject. Extra credit will be given if the student does a tool demo in class or demonstrates some other follow-up work on the subject.

Paper Reviews
For each student-led classroom session, all students need to upload brief reviews to Piazza by noon before class. Reviews are not expected for the instructor-led sessions. No late submission will be accepted with the following exception: there will be no penalty for up to 2 missed reviews during the semester. Reviews will be evaluated on the student's understanding of the subject.

Participation
In each class, students will be evaluated for their engagement, understanding and ideas. There will be no penalty for up to 2 "quiet" sessions during the semester.

Note for auditors
You will be required to present at least one paper in class. You can pick a paper from either the required or supplemental reading column in the schedule. Registered students will have priority for the choice of papers listed under required reading.

Tentative Schedule
Date Presenter Topic Required Reading
Supplemental Reading
Unit 1: Introduction, Logics, Proof Mechanics, Proof Engines
Aug-23 Roopsha Course Overview    
Aug-25 Roopsha Review: Propositional and First-order Logic BM:Ch1-3  
Aug-30 Roopsha Axiomatic Approach to Sequential Program Verification BM:Ch4 H69
Sep-1 Roopsha A Dash of Temporal Logic and Model Checking CES86  
Sep-6 Fei SAT Solving BM:Ch1.7, SLM08 GKSS08
Sep-8 Xilun SMT Solving BSST08 MB11
Sep-13 Fei MaxSAT LM08  
Sep-15 All Project Proposal Presentations    
Unit 2: Verification of Sequential Programs  
Sep-20 Hossein Bounded Model Checking BCCZ99  
Sep-22 Kiarash Interpolants and SAT-based Model Checking M03  
Sep-27 Xuankang Abstract Interpretation, Invariant Generation BM:Ch12  
Sep-29 Xilun/Sayali Abstraction-Refinement JM09 BMMR01,CGJLV03
Oct-4 David/Hui Concolic Execution GKK05 CS03
Oct-6 All Project Progress Review    
Oct-11   October Break    
Unit 3: Synthesis for Sequential Programs  
Oct-13 David Program Sketching STBSS06  
Oct-18 Gregory Proof-based Synthesis SGF10  
Oct-20 Hossein Programming by Example G10  
Oct-25 Nouraldin Programming via Statistical Language Models RVY14  
Oct-27 Roopsha Syntax-Guided Synthesis, Quantitative Program Repair A13, DSS16  
Nov-1 All Project Progress Review    
Unit 4: Verification of Concurrent Programs  
Nov-3 Roopsha Introduction, Challenges    
Nov-8 Kiarash Axiomatic Approach to Concurrent Program Verification OG76 L77
Nov-10 Xilun A Calculus of Atomic Actions EQT09  
Nov-15 Xuankang Partial-Order Reduction G90 D93
Nov-17 Gregory Predictive Analysis WKGG09  
Nov-22 Nouraldin Context-Bounded Reasoning QR05  
Nov-24   Thanksgiving Break    
Unit 5: Synthesis for Concurrent Programs  
Nov-29 Roopsha Synchronization Synthesis for Concurrent Programs VYY10, G15  
Dec-1 Roopsha Synchronization Synthesis for Concurrent Programs C15  
Dec-6 All Final Project Presentations    
Dec-8 All Final Project Presentations    
Course Material
We will use one textbook and read several papers in this seminar. 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