COS 516/ECE 516: Automated Reasoning about Software, Fall 2021

Course information

Semester: Fall 2021
Lectures: Monday & Wednesday 11:00 - 12:20pm
Location: McCosh Hall, room 66
Instructor: Zak Kincaid, zkincaid@cs.princeton.edu. Office hours: Monday 2-3pm, CS building room 219. (Starting 9/13)
Teaching assistant: Dongsheng Yang, dy5@princeton.edu. Office hours: Friday 2-3pm, Friend 010. (Starting 9/10)

Links: Canvas Calculus of Computation

Description

An introduction to algorithmic techniques for reasoning about software. Basic concepts in logic-based techniques including model checking, invariant generation, symbolic execution, and syntax-guided synthesis; automatic decision procedures in modern solvers for Boolean Satisfiability (SAT) and Satisfiability Modulo Theory (SMT); and their applications in automated verification, analysis, and synthesis of software. Emphasis on algorithms and automatic tools.

Schedule

This is a tentative schedule that may be changed during the course.
Links for reading material should be accessible from inside the Princeton network. Contact Zak Kincaid if you are having difficulty accessing resources.

Date Topics Readings Assignments
Sept 1 Introduction & Propositional logic. Bradley/Manna Ch 1
Sept 6 Labor day
Sept 8 SAT solving: DPLL and resolution.
Sept 13 SAT solving: CDCL. Marques-Silva, Lynce, Malik: SAT handbook, Chapter 4 PS1 due
Sept 15 Finite transition systems and BDDs. Bryant: Graph-Based Algorithms for Boolean Function Manipulation
Sept 20 First-order logic. Bradley/Manna Ch 2 PS2 due
Sept 22 First-order theories. Bradley/Manna Ch 3
Sept 27 SMT solving. De Moura, Bjørner: Satisfiability Modulo Theories: Introduction and Applications PS3 due
Sept 29 SMT solving. Barrett, Sebastiani, Seisha, Tinelli: SAT handbook, Chapter 26
Oct 4 Programs and operational semantics. Bradley/Manna Ch 4-6 PS4 due
Oct 6 Hoare logic. Hoare: An axiomatic basis for computer programming
Oct 11 Midterm review. PS5 due
Oct 13 Midterm exam.
Oct 18,20 Fall break
Oct 25 Semi-automated verification. Bradley/Manna Ch 12
Oct 27 Invariant inference I: control flow, Floyd's logic, and Houdini
Nov 1 Invariant inference II: data flow analysis Project outline due
Nov 3 Abstract interpretation.
Nov 8 Algebraic program analysis. Kincaid, Reps, Cyphert: Algebraic program analysis PS6 due
Nov 10 Software model checking I. Jhala, Majumdar: Software Model Checking
Nov 15 Software model checking II. PS7 due
Nov 17 Quantifiers and synthesis.
Nov 22 Temporal logic.
Nov 24 Thanksgiving break
Nov 29 Project presentations
Dec 1 Project presentations
Dec 6 Project presentations
Dec 14 Dean's date Project report due

Grading policies

Your final grade will be weighted as follows:
Component Weight
Problem sets 40%
Design Project 30%
Midterm Exam 25%
Participation 5%
We encourage you to attend the lectures and to participate actively in the course. These will be components of your Participation grade.

Late policy

Conduct

For homework and assignments, discussions with others are permitted, where the goal is to aid your understanding. However, the submitted work/code should be entirely your own.
For code submissions, please also submit a README file where you should name the individuals that you received help from or provided help to. Briefly mention the nature of the help you received or provided.
For the class project, you can work in teams of two. Discussions with your team-mate and with others are permitted.
For any of these (problem sets and class project), please DO NOT copy or get solutions from resources outside the course.
If you have any questions or concerns, please discuss these policies with the instructors.
Conduct during in-class exams is covered by the University Honor Code.