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

Course information

Semester: Fall 2025
Lectures: Monday & Wednesday 10:40 - 12:00pm
Location: Sherrerd Hall, Room 001
Instructor: Zak Kincaid, zkincaid@cs.princeton.edu. Office hours: Monday 1pm-2pm, 194 Nassau room 230
Teaching assistant: Nicolas Koh Office hours: Friday 10am-11am, CS 003

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.

and Binary Decision Diagrams.

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

Assignments are due at 11pm, with a 1 hour grace period.
Each assignment can be submitted a maximum of 5 days late. Late assignments will be penalized 10% per day late. Penalties for up to four late days are waived. If a student uses more than four late days, late passes will be applied to late work in order of total weight.
In case of special circumstances (e.g., illness, religious holidays, etc.), please write to zkincaid@cs.princeton.edu if you need an extension.

Conduct

For homework and assignments, discussions with others are permitted, where the goal is to aid your understanding. You may similarly make use of large language models (LLMs) like ChatGPT---for conceptual help only. 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.