Verification of Infinite-State Reactive Systems
Wednseday, 5:00-7:00 PM
Room 101, 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).
- Verifying invariance properties.
- Algorithmic construction of auxiliary invariants.
- Verifying progress properties.
- Parameterized systems.
- The CHAIN and WELL rules.
- Verifying progress under compassion.
- Verifying reactivity properties.