Wednesday, 5:00-7:00 PM

Room 709, 719 Broadway

- e-mail amir@cs.nyu.edu
- phone: (212) 998-3225
- office: 715 Broadway, Room 707
- office hours: Wednesday 2:00-4:00 PM, or by appointment

**Course requirements:**
Assignments and a term project.

** Textbooks:**

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

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.

- 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. 4, 2002: lecture1.ps, lecture1.pdf
- Lecture 2 -- Sept. 11, 2002: lecture2.ps, lecture2.pdf
- Lecture 3 -- Sept. 26, 2002: lecture3.ps, lecture3.pdf
- Lecture 4 -- Oct. 2, 2002: lecture4.ps, lecture4.pdf
- Lecture 5 -- Oct. 9, 2002, revised Oct. 30: lecture5.ps, lecture5.pdf
- Lecture 6 -- Oct. 16, 2002: lecture6.ps, lecture6.pdf
- Lecture 7 -- Oct. 23, 2002: lecture7.ps, lecture7.pdf
- Lecture 8 -- Oct. 30, 2002: lecture8.ps, lecture8.pdf
- Lecture 9 -- Nov. 6, 2002, revised Nov. 29, 2002: lecture9.ps, lecture9.pdf
- Lecture 10 -- Nov. 13, 2002: lecture10.ps, lecture10.pdf
- Lecture 11 -- Nov. 20, 2002: lecture11.ps, lecture11.pdf
- Executable package for the Solaris system on Sun computers -- tlvsun.zip.
- Executable package for Linux -- tlvlinux.zip.
- TLV Manual -- tlv-manual.ps.
- TLV Tutorial -- tlv-tutorial.ps