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

Related Areas:

• Cyber-Physical Systems and Design Automation (CPSDA)

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: Student Option

Final Exam Status: No

---

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

Class Notes
Phase 1 and 2 seats are open to EECS Grad students. Remaining seats open during the adjustment period.

**Enrollment Permission seats are reserved for internal programs and are not open. Please DO NOT email the instructor or scheduling to request a seat**

Links:

• EECS Course Archives (CalNet authentication required)
• CS enrollment policies
• EE enrollment policies
• HKN course maps