Catalog Description: Introduction to the theory and practice of formal methods for the design and analysis of systems, with a focus on algorithmic techniques. Covers selected topics in computational logic and automata theory including modeling and specification formalisms, temporal logics, satisfiability solving, model checking, synthesis, learning, and theorem proving. Applications to software and hardware design, cyber-physical systems, robotics, computer security, and other areas will be explored as time permits.

Units: 3

Prerequisites: Graduate standing or consent of instructor; COMPSCI 170 is recommended.

Formats:
Spring: 3.0 hours of lecture per week
Fall: 3.0 hours of lecture per week

Grading basis: letter

Final exam status: No final exam

---

Class Schedule (Spring 2025):
EECS 219C – MoWe 13:00-14:29, Cory 299 – Sanjit A Seshia

Class homepage on inst.eecs

Related Areas:

• Cyber-Physical Systems and Design Automation (CPSDA)