Verification of Reactive Systems
Thursday, 5:00-7:00 PM
Room 613, Warren Weaver Hall
Professor Amir Pnueli
Prerequisites: Some background in
algorithm design, familiarity with the language of first-order logic,
and parallel programs.
- phone: (212) 998-3225
- office: 715 Broadway, Room 707
- office hours: Wednesday 2:00-4:00, or by appointment
Assignments and a
Recommended: Temporal Verification of Reactive Systems: Safety
by Zohar Manna and Amir Pnueli, Springer-Verlag
- 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 construction of temporal testers.
- Checking an FDS for feasibility -- the graph theoretic formulation.
- Model checking LTL properties of systems.
- Binary decision diagrams (BDD's).
- Symbolic LTL model checking -- the TLV verification system.
- Symbolic model checking of infinite-state systems, using
abstraction and composition.