CS 256 Formal Methods for Reactive Systems

Concurrent and reactive systems are parallel programs that maintain an ongoing interaction with their environment. Examples include operating systems, hardware devices, reservation systems, communication protocols, web servers, air traffic and automobile control systems, and, in general, all embedded systems.

Many of these programs play a critical role in the correct operation of equipment and services so that even small program errors can have disastrous consequences, including loss of lives. Yet these programs are notoriously hard to get correct. Programming them is extremely difficult because of the parallelism involved, while exhaustive testing is impossible due to a generally infinite number of distinct environment conditions.

CS256 introduces the logical foundations to reason about these systems. Specification languages include temporal logics — LTL (linear time) and CTL (branching time) — and automata over infinite strings and trees. We concentrate on giving a firm theoretical basis for the most important verification techniques: deductive (theorem proving), algorithmic (model checking), and their (state-of-the-art) combination.

The basics of mathematical logic, such as CS156, CS157, Phil160a, CS103 or equivalent, and familiarity with an Algol-like language (Pascal, C, Java ...) Previous experience with finite-state automata is useful, but not required, for some parts of the course.

• Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety, Springer 1995. (AKA The Green Book)
  This is the main textbook and contains about 2/3 of the syllabus.
• Copies of lecture slides will be given before each lecture and made available on this web site.
• We will suggest additional books and research papers on specific topics (not required) during the course.