Analysis of Reactive Systems, Algorithmic and Deductive Methods

Thursday, 5:00-6:50 PM
Room 317, CIWW
Amir Pnueli

Reaching Me

Amir Pnueli

Class list

All students should register themselves with the class list, which is used for all technical discussions concerning the course and the course project. To subscribe to this list visit the web page:

where you will find full directions.

Please send all your questions to this list (not only to the instructor) so that everyone can participate.

Prerequisites: Some background in algorithm design, familiarity with the language of first-order logic, and parallel programs.

Course requirements: Assignments and a term project.

Recommended: "Temporal Verification of Reactive Systems: Safety" by Zohar Manna and Amir Pnueli, Springer-Verlag.

"Model Checking", by E.C. Clarke and O. Grumberg and D. Peled, MIT Press, 2000.

Course Description

Reactive systems are systems whose role is to maintain an ongoing interaction with their environment rather than produce some final value upon termination. Typical examples of reactive systems are Air traffic control system, Programs controlling mechanical devices such as a train, a plane, or ongoing processes such as a nuclear reactor.

The Formal Methods approach to software construction is based on viewing a program and its execution as mathematical objects and applying mathematical and logical techniques to specify and analyze the properties and behavior of these objects. The main advantages of the formal approach to software construction is that, whenever applicable, it can lead to an increase of the reliability and correctness of the resulting programs by several orders of magnitude.

Several approaches to the verification of reactive systems are available, the most prominent of which are Algorithmic (model checking) and Deductive verification. In this semester we will consider both of these approaches. Under algorithmic verification we will show how to verify properties of finite-state systems. Under deductive verification, we use theorem-proving techniques to establish the correctness of infinite-state reactive programs relative to their temporal specifications. We will be using computer-aided theorem provers such as CVC, PVS or STeP for verifying the properties of programs.

Towards the end of the semester, we will consider the use of the notions of reactive systems, their specification, and verification for the modeling of Biological systems at a certain level of abstraction.

Course topics:

Class Presentations



Term Project