A decision procedure.
Drawing by Ilya Yodovsky Jr., from Decision Procedures: An Algorithmic Point of View by Daniel Kroening and Ofer Strichman

Welcome to CSE290Q, fall 2019 edition!

SAT and SMT solvers are now widely used across many areas of computer science, especially for automated software and hardware verification, but they are often “black boxes” to their users. This course is for those who want to look under the hood to learn how solvers work, and to explore a variety of systems that make use of them.

For more information, read the first-day-of-class course overview, then check out the reading list.