Computer Science 597B: Advanced Topics in Computer Science
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: Tue Th, 1:30 PM -- 2:50 PM, CS Building 104
Professor: Aarti Gupta, CS Building 220, 258-8017, firstname.lastname@example.org
Office Hours: Wed 11:00 -- 11:50 AM or by appointment, CS Building 220
Assistant Instructor: Yakir Vizel, EQuad C-305, 258-7035, email@example.com
Office Hours: by appointment
Graduate Coordinator: Nicki Gotsis, CS Building 310, 258-5387, firstname.lastname@example.org
Prerequisites: COS 126, or you should have substantial programming experience using some high-level programming language such as Java or C.
For about half of the course:
The Calculus of Computation: Decision Procedures with Applications to Verification
by Aaron R. Bradley and Zohar Manna
Announcements and Discussions
Listed in schedule, related to lectures.
Course announcements, discussions, and questions are available on Piazza.
Please study the course Policies, and check with the Professor if you have any questions.