Formal Methods for Reactive Systems

CS256, Winter 2009, Stanford University

Assignments (always due Wed's at the start of class)

Assignment 1 (due Wednesday, Jan 14)

Assignment 2 (due Wednesday, Jan 21)

Assignment 3 (due Wednesday, Jan 28)

Assignment 4 (due Wednesday, Feb 4)

Assignment 5 (due Wednesday, Feb 11)

Assignment 6

Assignment 7

Assignment 8

Click here for documents (slides, etc.)

Textbook chapters covered



MonWed 11:00–12:15
First meeting Wednesday, Jan 7


Gates B12


Zohar Manna
Office: Gates 481
Office hours: by appointment

Teaching assistant:

Boyu Wang
Office: Durand 104
Office hours: Tuesday, Friday 3pm–5pm Durand 1st floor lounge


Wendy Cardamone
Office: Gates 461
Phone: 725-2340

Mailing list:

All students registered for the class should be automatically on the class mailing list. Email Boyu to be added to the list if you are auditing (or if you later drop the class and want to be kept on the list).


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.


Weekly homeworks + final exam. There will be no midterm.
Collaboration: no collaboration on homeworks or exam unless otherwise specified.

Final examination:

Wednesday, Mar 11, 11:00am–2:00pm in Gates 260. The exam is open book and open notes and closed laptop. Please plan to arrive at least 15min early.

Mon Jan 5 20:13:02 2009