Lecture, four hours; outside study, eight hours. Requisite: course 181. Introduction to theory and practice of formal methods for design and analysis of concurrent and embedded systems, with focus on algorithmic techniques for checking logical properties of hardware and software systems. Topics include semantics of reactive systems, invariant verification, temporal logic model checking, theory of omega automata, state-space reduction techniques, compositional and hierarchical reasoning. Letter grading.