Wednesday, 5:00-6:50 PM

Room 513, CIWW

- e-mail amir@cs.nyu.edu
- phone: (212) 998-3225
- office: CIWW, Room 505
- 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. 5, 2007: slides (lecture1.ps) , lecture1.pdf, lecture1_h4.ps , lecture1_h4.pdf
- Lecture 2 -- Sept. 19, 2007: slides (lecture2.ps) , lecture2.pdf, lecture2_h4.ps , lecture2_h4.pdf
- Lecture 3 -- Sept. 26, 2007: slides (lecture3.ps) , lecture3.pdf, lecture3_h4.ps , lecture3_h4.pdf
- Lecture 4 -- Sept. 28, 2007: slides (lecture4.ps) , lecture4.pdf, lecture4_h4.ps , lecture4_h4.pdf
- Lecture 5 -- Oct. 3, 2007: slides (lecture5.ps) , lecture5.pdf, lecture5_h4.ps , lecture5_h4.pdf
- Lecture 6 -- Oct. 17, 2007: slides (lecture6.ps) , lecture6.pdf, lecture6_h4.ps , lecture6_h4.pdf
- Lecture 7 -- Oct. 19, 2007: slides (lecture7.ps) , lecture7.pdf, lecture7_h4.ps , lecture7_h4.pdf
- Lecture 8 -- Nov. 8, 2007: slides (lecture8.ps) , lecture8.pdf, lecture8_h4.ps , lecture8_h4.pdf
- Lecture 9 -- Nov. 15, 2007: slides (lecture9.ps) , lecture9.pdf, lecture9_h4.ps , lecture9_h4.pdf
- Lecture 10 -- Nov. 28, 2007: slides (lecture10.ps) , lecture10.pdf, lecture10_h4.ps , lecture10_h4.pdf
- Lecture 11 -- Dec. 12, 2007: slides (lecture11.ps) , lecture11.pdf, lecture11_h4.ps , lecture11_h4.pdf

- Assignment 1 -- ass1.ps, ass1.pdf. Due 11.14.07
- Assignment 2 -- ass2.ps, ass2.pdf. Due 11.27.07
- Assignment 3 -- ass3.ps, ass3.pdf. Due 12.21.07

- Files -- token-long.smv.
- Files -- leader.smv.
- Files -- deductive.tlv.
- Files -- prod-cons.smv.
- Files -- petn.smv.