Advanced Topics in Reactive Verification
G22.3033-017
Thursday, 5:00-6:50 PM
Room 513 WWH
Amir Pnueli
Reaching Me
Amir Pnueli
- 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 Description
This course studies in greater depth various topics in the field of
program verification. It assumes prior knowledge of temporal logic, model
checking and deductive verification. Among the topics to be considered, we
will consider:
- 1. The unified logic CTL*, its model checking and deductive verification.
- 2. Methods for parameterized verification, including "regular model
checking", "network invariants", "counter abstraction", and "invisible
auxiliary constructs".
- 3. Abstraction-aided verification -- soundness and completeness of the
method.
- 4. Predicate abstraction and abstraction refinement.
- 5. Methods for program synthesis from temporal specification.
As part of the course work, students will be required to import,
install, and demonstrate one of the available verification tools for model
checking or deductive verification of reactive, real-time, or hybrid
systems.
Prerequisites:
Some background in algorithm design, familiarity with the language of
first-order logic, and knowledge of compiler construction techniques.
Course requirements:
Assignments and a term project. Importing, installing, and presenting,
one of the publicly available system analysis tools.
Class Presentations
-
Lecture 1 -- Jan. 22, 2004:
lecture1.ps,
lecture1.pdf
-
Lecture 2 -- Jan. 29, 2004:
lecture2.ps,
lecture2.pdf
-
Lecture 3 -- Feb. 5, 2004:
lecture3.ps,
lecture3.pdf
-
Lecture 4 -- Feb. 12, 2004:
lecture4.ps,
lecture4.pdf
-
Lecture 5 -- Feb. 19, 2004:
lecture5.ps,
lecture5.pdf
-
Lecture 6 -- Feb. 26, 2004:
lecture6.ps,
lecture6.pdf
-
Lecture 7 -- March 4, 2004:
lecture7.ps,
lecture7.pdf
-
Lecture 8 -- March 18, 2004:
lecture8.ps,
lecture8.pdf
-
Lecture 9 -- April 7, 2004:
lecture9.ps,
lecture9.pdf,
Counter_Abstraction.ppt
-
Lecture 10 -- April 22, 2004:
lecture10.ps,
lecture10.pdf
Term Project