Computer-Aided Reasoning for Software

UW CSEP 590B, Spring 2026

Welcome to CARS. Solvers, the engines behind SAT and SMT, can do remarkable things: find bugs that testing misses, synthesize code from specifications, verify critical properties, and explore design spaces automatically. Most software engineers never learn to wield them. This quarter you will study how solvers work under the hood, then build solver-aided tools and techniques that put them to work. It is a different kind of engineering, and we cannot wait to dig into it with you.

Staff

Office Hours