CS590: Reasoning about Programs

Instructor Roopsha Samanta
Class Tuesday and Thursday, 4:30-5:45pm, Forney 1043
Office hours Tuesday, 3:30-4:30pm (or by appointment), LWSN 2116L
TA Anshu Maheshwari
TA Office hours Friday, 12:00-1:00pm (or by appointment), HAAS G50
Online forum Piazza (sign up here)
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, Propositional Logic  
Aug-24 First-order Logic BM:Ch1-2
Aug-29 First-order Theories BM:Ch3
Aug-31 Hoare Logic I BM:Ch4, H69
Sep-5 Hoare Logic II
Sep-7 SAT Solving BM:Ch1.7, GKSS08, SLM08,
Sep-12 SMT Solving, Congruence Closure for EUF BSST08, MB11, BM:Ch9
Unit 2: Sequential Programs: Verification and Analysis
Sep-14 Invariant Generation BM:Ch12Project Proposal
Sep-19 Review HW 1
Sep-21 Bounded Model Checking BCCZ99, CKY03
Sep-26 Abstraction-Refinement JM09, BMMR01, HJMS02, CGJLV03,HW 2
Unit 3: Concurrent Programs: Verification and Analysis
Sep-28 Introduction, Owicki-Gries Approach OG76, L77
Oct-3 Midterm
Oct-5 Bounded Analyses, Predictive Analysis QR05,WKGG09
Oct-10 October Break  
Unit 4: Program Synthesis
Oct-12 Introduction G10,A13,BJ13HW 3
Oct-17 Inductive Synthesis, Explicit Search
Oct-19 Structured Explicit Search using Version Spaces (Flashfill) G11,HG12,SG12,GHS12
Oct-24 Constraint-based Search (Sketch, CEGIS) STBSS06
Oct-26 Constraint-based Search (Component, Proof-based Synthesis) GJTV11,JGST10,SGF10Project Progress
Oct-31 Machine Learning-based Synthesis (JSNice) RVK15
Nov-2 Machine Learning-based Synthesis (Neural synthesis) P17
Nov-7 Synthesis for Concurrency VYY10,G15,C15
Nov-9 Synthesis Fest
Nov-14 Synthesis Fest
Nov-16 Synthesis Fest
Nov-21 No class
Nov-23 Thanksgiving Break  
Nov-28 Wrap-up
Nov-30 Final Project Presentations
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.
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.
Synthesis Fest
PBE
AGK13 Aws Albarghouthi, Sumit Gulwani and Zachary Kincaid Recursive Program Synthesis. CAV 2013
ZS13 Sai Zhang, Yuyin Sun Automatically Synthesizing SQL Queries from Input-Output Examples ASE, 2013
PGGP14 Daniel Perelman, Sumit Gulwani, Dan Grossman and Peter Provost Test-Driven Synthesis. PLDI 2014
LSL15 Alan Leung, John Sarracino, Sorin Lerner Interactive Parser Synthesis by Example PLDI, 2015
FCD15 John K. Feser, Swarat Chaudhuri, Isil Dillig Synthesizing Data Structure Transformations from Input-Output Examples. PLDI 2015
YKDC16 Navid Yaghmazadeh, Christian Klinger, Isil Dillig, Swarat Chaudhuri Synthesizing Transformations on Hierarchically Structured Data. PLDI 2016
WDS17 Xinyu Wang, Isil Dillig, Rishabh Singh Synthesis of Data Completion Scripts using Finite Tree Automata OOPSLA, 2017
ASV17 Loris D’Antoni, Rishabh Singh, Michael Vaughn NoFAQ: Synthesizing Command Repairs from Examples FSE, 2017
WCB17 Chenglong Wang, Alvin Cheung, Rastislav Bodik Synthesizing Highly Expressive SQL Queries from Input-Output Examples PLDI, 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
WDS17 Xinyu Wang, Isil Dillig, Rishabh Singh Synthesis of Data Completion Scripts using Finite Tree Automata OOPSLA 2017
PBE for Excel
SG12 Rishabh Singh, Sumit Gulwani Synthesizing number transformations from input-output examples. CAV 2012
LG14 Vu Le, Sumit Gulwani FlashExtract: A Framework for Data Extraction by Examples. PLDI 2014
PG15 Oleksandr Polozov, Sumit Gulwani FlashMeta: A Framework for Inductive Program Synthesis. OOPSLA 2015
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
Synthesis for Concurrency/Distributed Systems
H12 Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin Rinard, Mooly Sagiv Concurrent Data Representation Synthesis PLDI, 2012
U13 Abhishek Udupa, Arun Raghavan, Jyotirmoy V. Deshmukh, Sela Mador-Haim, Milo M. K. Martin, Rajeev Alur TRANSIT: Specifying Protocols with Concolic Snippets. PLDI 2013
M15 Jedidiah McClurg, Hossein Hojjat, Pavol Cerny, Nate Foster Efficient Synthesis of Network Updates PLDI, 2015
SA16 Calvin Smith, Aws Albarghouthi MapReduce Program Synthesis PLDI, 2016
FN17 Azadeh Farzan, Victor Nicolet Synthesis of Divide and Conquer Parallelism for Loops PLDI, 2017
Type-directed synthesis
KMPS10 Viktor Kuncak, Mikael Mayer, Ruzica Piskac, and Philippe Suter. Complete functional synthesis. PLDI 2010
OZ15 Peter-Michael Osera and Steve Zdancewic. Type-and-Example-Directed Program Synthesis. PLDI 2015
P12 Daniel Perelman, Sumit Gulwani, Thomas Ball and Dan Grossman. Type-Directed Completion of Partial Expressions. PLDI 2012
PKS16 Nadia Polikarpova, Ivan Kuraj, Armando Solar-Lezama. Program Synthesis from Polymorphic Refinement Types. PLDI 2016
F17 Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, Thomas W. Reps Component-Based Synthesis for Complex APIs POPL, 2017
Other Synthesis Paradigms
B10 Shaon Barman, Rastislav Bodík, Satish Chandra, Joel Galenson, Doug Kimelman, Casey Rodarmor, Nicholas Tung Programming with Angelic Nondeterminism POPL, 2010
CCL14 Swarat Chaudhuri, Martin Clochard, Armando Solar-Lezama Bridging Boolean and Quantitative Synthesis Using Smoothed Proof Search POPL, 2014
TB14 Emina Torlak, Ras Bodik. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages.PLDI, 2014
ACR15 Rajeev Alur, Pavol Cerny, Arjun Radhakrishna Synthesis through Unification. CAV 2015
BTGC16 James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze Optimizing Synthesis with Metasketches. POPL, 2016
G17 Adria Gascon, Ashish Tiwari, Brent Carmer, Umang Mathur Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis CAV, 2017
ML/NLP/Probabilistic programs
M13 Aditya Krishna Menon, Omer Tamuz, Sumit Gulwani, Butler Lampson, Adam Tauman Kalai A Machine Learning Framework for Programming by Example. ICML 2013
NORV15 Aditya V. Nori, Sherjil Ozair, Sriram K. Rajamani, and Deepak Vijaykeerthy. Efficient Synthesis of Probabilistic Programs. PLDI 2015
D16 Aditya Desai, Sumit Gulwani, Vineet Hingorani, Nidhi Jain , Amey Karkare, Mark Marron, Sailesh R, Subhajit Roy Program Synthesis Using Natural Language. ICSE 2016
LMN16 Christof Loding, P. Madhusudan, and Daniel Neider. Abstract Learning Frameworks for Synthesis. TACAS 2016.
RBVK16 Veselin Raychev, Pavol Bielik, Martin Vechev and Andreas Krause. Learning Programs from Noisy Data. POPL, 2016.
SS16 Susmit Jha, Sanjit A. Seshia. A Theory of Formal Synthesis via Inductive Learning. Arxiv, 2016.
GPS17 Patrice Godefroid, Hila Peleg, Rishabh Singh Learn&Fuzz: Machine Learning for Input Fuzzing. ASE 2017
Y17 Navid Yaghmazadeh, Yuepeng Wang, Isil Dillig, Thomas Dillig SQLizer: Query Synthesis from Natural Language OOPSLA, 2017
S17 Mark Santalucito, Ennan Zhai, Rahul Dhodapkar, Aaron Shim, Ruzica Piskac Synthesizing Configuration File Specifications with Association Rule Learning. OOPSLA, 2017
Misc. Applications
M05 David Mandelin, Lin Xu, Rastislav Bodik, Doug Kimelman Jungloid Mining: Helping to Navigate the API Jungle PLDI, 2005
SJR08 Armando Solar-Lezama, Christopher Grant Jones, Rastislav Bodik. Sketching Concurrent Data Structures.Proceedings of PLDI 2008
TGT09 Ankur Taly, Sumit Gulwani, Ashish Tiwari Synthesizing switching logic using constraint solving STTT - VMCAI 2009
SS11 Rishabh Singh, Armando Solar-Lezama. Synthesizing Data-structure Manipulations from Storyboards. FSE 2011
SGS13 Rishabh Singh, Sumit Gulwani, Armando Solar-Lezama Automated Feedback Generation for Introductory Programming Assignments PLDI, 2013
K13 Ali Sinan Koksal, Yewen Pu, Saurabh Srivastava, Rastislav Bodik, Jasmin Fisher, Nir Piterman Synthesis of Biological Models from Mutation Experiments POPL, 2013
G14 Joel Galenson, Philip Reames, Rastislav Bodik, Björn Hartmann, Koushik Sen CodeHint: Dynamic and Interactive Synthesis of Code Snippets ICSE, 2014
F15 Jasmin Fisher, Ali Sinan K¨oksal, Nir Piterman, Steven Woodhouse Synthesising Executable Gene Regulatory Networks from Single-cell Gene Expression Data CAV, 2015
K17 Martin Kucera, Petar Tsankov, Timon Gehr, Marco Guarnieri, Martin Vechev Synthesis of Probabilistic Privacy Enforcement ACM CCS, 2017
QL17 Xiaokang Qiu, Armando Solar-Lezama Natural Synthesis of Provably-Correct Data-Structure Manipulations OOPSLA, 2017
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.”
Related courses