UW CSE 507

Computer-Aided Reasoning for Software

CSE 507 is a graduate level introduction to research in 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!

Lecture

Tue / Thu at 10 a.m.
CSE2 Room G04
Recordings
Code, slides

Staff

Zachary Tatlock

PLSE 13th Year Faculty Member

Office Hours: Fri 11 a.m., CSE2 201

Audrey Seo

PLSE 6th Year PhD Student

Office Hours: Tuesdays and Thursdays 2:30-3:30 p.m. in the PLSE lab (CSE2 253)

Credits

All the fantastic materials for CSE 507 (slides, homework assignments, etc.) were originally designed and developed by Emina Torlak.

Page updated