Princeton University Computer Science Department

COS 516 / ELE 516 Automated Reasoning about Software Aarti Gupta

Fall 2017

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, 1:30-2:50 PM, Sherrerd Hall 001

Professor: Aarti Gupta, CS Building 220, 258-8017, aartig@cs.princeton.edu

Office Hours: Wed 11:00 AM - 12:00 PM, CS Building 220

Teaching Assistant: Lauren Pick, lpick@princeton.edu

Office Hours: Tues 1:30-2:30 PM, Thurs 3:30-4:30 PM, Friend Center 010

Graduate Coordinator: Nicki Gotsis, CS Building 310, 258-5387, ngotsis@cs.princeton.edu

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

Resources

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

Listed in schedule, related to lectures.

Course announcements, discussions, and questions are available on Piazza.

Academic Regulations

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