Monday, 5:00-6:50 PM

Room 102, WWH

- e-mail amir@cs.nyu.edu
- phone: (212) 998-3225
- office: WWH, Room 505
- office hours: Monday 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.

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

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 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).
- Branching-time temporal logic CTL*.
- Finite-State Systems and their Verification (Model Checking).
- A programmable model checker TLV.
- Model checking CTL* formulas.
- 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 -- January 23, 2006: lecture1.ps, lecture1.pdf
- Lecture 2 -- January 30, 2006: lecture2.ps, lecture2.pdf
- Lecture 3 -- February 6, 2006: lecture3.ps, lecture3.pdf
- Lecture 4 -- February 13, 2006: lecture4.ps, lecture4.pdf
- Lecture 5 -- February 27, 2006: lecture5.ps, lecture5.pdf
- Lecture 6 -- March 6, 2006: lecture6.ps, lecture6.pdf
- Lecture 7 -- March 20, 2006: lecture7.ps, lecture7.pdf
- Lecture 8 -- March 30, 2006: lecture8.ps, lecture8.pdf
- Lecture 9 -- April 6, 2006: lecture9.ps, lecture9.pdf
- Lecture 10 -- April 10, 2006: lecture10.ps, lecture10.pdf
- Lecture 11 -- May 1, 2006: lecture11.ps, lecture11.pdf

- TLV Home Page
**TLV**. Obtain there the TLV object code, TLV Manual and TLV Tutorial. - SMV Manual -- SMV_manual.pdf. More detailed information is available in the book "Symbolic Model Checking" By K.L. McMillan, Kluwer Academic Publishers, 1993.
- Files -- try1.smv and try1.pf.
- Files -- try2.smv and try2.pf.
- Files -- try3.smv and try3.pf.
- Files -- pet2.smv and pet2.pf.
- File -- skeleton.pf.
- File -- deductive.tlv. Use this version of file "deductive.tlv" for the term project.