Deductive Verification of Reactive Systems
Wednesday, 5:00-6:50 PM
Room 513, CIWW
Prerequisites: Some background in
algorithm design, familiarity with the language of first-order logic,
and parallel programs.
- phone: (212) 998-3225
- office: CIWW, Room 505
- office hours: Wednesday 2:00-4:00 PM, or by appointment
Assignments and a term project.
Recommended: Temporal Verification of Reactive Systems: Safety
by Zohar Manna and Amir Pnueli, Springer-Verlag
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
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.
- The computational model of Fair Discrete Systems (FDS).
- A simple programming language (SPL) and its translation into FDS.
- The specification language of linear temporal logic (LTL).
- The PVS Theorem prover. Encoding FDS's and LTL within PVS.
- Verifying invariance properties.
- Algorithmic construction of auxiliary invariants.
- Verifying progress properties.
- The CHAIN and WELL rules.
- Verification Diagrams.
- Verifying progress under compassion.
- Verifying general LTL properties.
Lecture 1 -- Sept. 5, 2007:
slides (lecture1.ps) ,
Lecture 2 -- Sept. 19, 2007:
slides (lecture2.ps) ,
Lecture 3 -- Sept. 26, 2007:
slides (lecture3.ps) ,
Lecture 4 -- Sept. 28, 2007:
slides (lecture4.ps) ,
Lecture 5 -- Oct. 3, 2007:
slides (lecture5.ps) ,
Lecture 6 -- Oct. 17, 2007:
slides (lecture6.ps) ,
Lecture 7 -- Oct. 19, 2007:
slides (lecture7.ps) ,
Lecture 8 -- Nov. 8, 2007:
slides (lecture8.ps) ,
Lecture 9 -- Nov. 15, 2007:
slides (lecture9.ps) ,
Lecture 10 -- Nov. 28, 2007:
slides (lecture10.ps) ,
Lecture 11 -- Dec. 12, 2007:
slides (lecture11.ps) ,