Thursday, 5:00-6:50 PM

Room 317, CIWW

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

http://www.cs.nyu.edu/mailman/listinfo/g22_3033_011_fa09

where you will find full directions.

Please send all your questions to this list (not only to the instructor) so that everyone can participate.

**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 CVC, PVS or STeP for verifying the properties of programs.

Towards the end of the semester, we will consider the use of the notions of reactive systems, their specification, and verification for the modeling of Biological systems at a certain level of abstraction.

- 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).
- Finite-State Systems and their Verification (Model Checking).
- A programmable model checker TLV.
- 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.
- Modeling Biological Systems as Reactive Systems.

- Lecture 1 -- September 10, 2009: slides (lecture1.ps) , lecture1.pdf, lecture1_h4.ps , lecture1_h4.pdf
- Lecture 2 -- September 17, 2009: lecture2.ps, lecture2.pdf, lecture2_h4.ps , lecture2_h4.pdf
- Lecture 3 -- September 24, 2009: lecture3.ps, lecture3.pdf lecture3_h4.ps , lecture3_h4.pdf
- Lecture 4 -- October 1, 2009: lecture4.ps, lecture4.pdf lecture4_h4.ps , lecture4_h4.pdf
- Lecture 5 -- October 15, 2009: lecture5.ps, lecture5.pdf lecture5_h4.ps , lecture5_h4.pdf
- Lecture 6 -- October 22, 2009: lecture6.ps, lecture6.pdf lecture6_h4.ps , lecture6_h4.pdf
- Lecture 7 -- November 5, 2009: lecture7.ps, lecture7.pdf, lecture7_h4.ps, lecture7_h4.pdf
- Lecture 8 -- November 12, 2009: lecture8.ps, lecture8.pdf, lecture8_h4.ps , lecture8_h4.pdf
- Lecture 9 -- November 19, 2009: lecture9.ps, lecture9.pdf, lecture9_h4.ps, lecture9_h4.pdf
- Lecture 10 -- December 3, 2009: lecture10.ps, lecture10.pdf, lecture10_h4.ps, lecture10_h4.pdf
- Lecture 11 -- December 10, 2009: lecture11.ps, lecture11.pdf, lecture11_h4.ps, lecture11_h4.pdf
- Lecture 12 -- December 15, 2009: lecture12.pdf, lecture12_h4.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.
- Files -- token-long.smv.
- Files -- leader.smv.
- File -- skeleton.pf.
- File -- deductive.tlv. Use this version of file "deductive.tlv" for the term project.

- Assignment 1 -- ass1.ps, ass1.pdf. Due 10.8.09
- Assignment 2 -- ass2.ps, ass2.pdf. Due 10.22.09
- Assignment 3 -- ass3.html, Due 11.19.09
- Assignment 4 -- ass4.html, Due 11.30.09
- Assignment 5 -- ass5.html, Due 12.19.09

- Term Project -- project.html, Due 12.23.09