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 |
Communication