Computer-Aided Reasoning for Software

CSE 507 course is a graduate level introduction to automated reasoning techniques and their application in tools for the design, analysis, and construction of software. In the first half of the course, we will survey the logical foundations and algorithms behind SAT solvers, SMT solvers, and finite model finders. In the second half of the course, we will apply these techniques to automatic bug finding, program verification, and program synthesis. As a student in this course, you will learn how solvers work, and how to use them to build cool programming tools!

Meetings and Staff

Lectures CSE 403, WF 9:30-10:50
Instructor Emina Torlak (emina@cs), CSE 596, Th 9:00-10:00
TA James Bornholt (bornholt@cs), CSE 218, F 11:00-12:00


cse507-staff@cs Contact the staff.
cse507a_wi17@uw Class mailing list.
Dropbox Assignment dropbox.
Gradebook Course grade database.
Feedback Contact the instructor anonymously.