![]() Princeton University
|
COS 516 / ELE 516
|
Fall 2020 |
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.
Lectures: Mon Wed, 11:00 AM -- 12:20 PM, Location: on Zoom
Professor: Aarti Gupta (aartig), CS Building 220, 258-8017
Office Hours: TBD, on Zoom
Teaching Assistants: Divya Raghunathan (dr31), Zexuan Zhong (zzhang)
Graduate Coordinator: Nicki Gotsis (ngotsis), CS Building 310, 258-5387
Prerequisites: COS 226 and COS 326 (or equivalent programming experience)
Textbook
PapersFor about half of the course:
The Calculus of Computation: Decision Procedures with Applications to Verification
by Aaron R. Bradley and Zohar Manna
Electronic version
Lectures, Homeworks, ProjectsListed in schedule, related to lectures.
Announcements and DiscussionsAvailable on the Canvas course website
Slides posted before each lecture
Video recordings of lectures (Zoom sessions) posted after each lecture
Please see the Policies regarding Class Recording.
Course announcements, discussions, and questions are available on the Ed Discussion forum.
Please study the course Policies, and check with the Professor if you have any questions.