CS 292C: Computer-Aided Reasoning for Software

This is a graduate-level introduction to automated reasoning techniques and their application in tools for the design, analysis, and synthesis of software. In the first half of the course, we will study the logical foundations and algorithms behind modern 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 leverage state-of-the-art program analyzers and synthesizers (e.g., Rosette, Neo, etc) to build cool tools!