Analysis of Reactive Systems

G22.3033-004
Wednesday, 5:00-7:00 PM
Room 709, 719 Broadway
Amir Pnueli

Reaching Me

Amir Pnueli

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

Course requirements: Assignments and a term project.

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

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. This semester we concntrate on deductive verification, where we use theorem-proving techniques to establish the correctness of reactive programs relative to their temporal specifications. We will be using computer-aided theorem provers such as PVS and STeP for verifying the properties of programs.

Course topics:

Class Presentations