Current Teaching:

CSE 293: Introduction to Formal Methods (Winter 2020; MWF 4-5:05)

Formal methods are a set of mathematical techniques for modeling, designing, and analyzing systems to obtain rigorous guarantees about their behavior. These include ways to prove that a system is correct under all possible inputs, or to automatically synthesize correct systems from high-level specifications of what they should do. This course will survey a range of fundamental formal methods techniques for modeling, specification, verification, synthesis, and testing, highlighting applications to hardware and software design, cybersecurity, robotics, autonomous systems, and machine learning. The course will include a project where students will apply formal methods to a problem in a field of their choice. Primary topics we will cover include logical formalisms, SAT/SMT solving, model checking, program synthesis, symbolic execution, and test generation. According to student interest, we will also cover a selection of advanced topics such as modeling of cyber-physical systems, temporal logic falsification, and verification of neural networks.

Prerequisites: Students should be familiar with propositional (Boolean) logic, finite automata, the complexity classes P and NP, and basic graph algorithms. Feel free to contact the instructor with any questions about taking the course.