Course Summary

This course provides an introduction to algorithmic techniques for reasoning about software. Students will learn the basics of modern Boolean Satisfiability (SAT) solvers and Satisfiability Modulo Theory (SMT) solvers, and their applications in techniques for verification, analysis, and synthesis of software. The course covers techniques like model checking, invariant generation, symbolic execution, and syntax-guided synthesis.

---

Administrative Information

Lectures: Mon Wed, 11:00am--12:20pm ET, Location: Andlinger 017 Friend Center (FC) 009

Professor: Aarti Gupta (aartig), CS Building 220, 258-8017

• Office Hours: Tue 4:00--5:00pm ET, CS 220

Teaching Assistant: Mike He (dh7120)

• Office Hours: Wed and Thu, 4:00--5:00pm ET, CS 003 (basement of the CS building)

Graduate Coordinator: Nicki Mahler (ngotsis), 131 Friend Center, 258-5387

Prerequisites: COS 226 and COS 326 (or equivalent programming experience)

---

Resources

Textbook

For about half of the course:
The Calculus of Computation: Decision Procedures with Applications to Verification
by Aaron R. Bradley and Zohar Manna
Electronic version

Papers

Listed in schedule, related to lectures.

Lectures, Homeworks, Projects

Available on the Canvas course website
Slides posted before each lecture

Announcements and Discussions

Course announcements, discussions, and questions are available on the Ed Discussion forum.

---

Academic Regulations

Please study the course Policies, and check with the Professor if you have any questions.