• Discrete-Systems Syllabus

Course Content

1. Automata: deterministic, nondeterministic, and alternating.
2. Transition Systems, and their symbolic representation
3. Alternation and 2-player game structures
4. Ticc, a language and system for component modeling
5. Safety and reachability verification: enumerative, symbolic, SAT-based, simulation-based
6. System Relations: simulation and bisimulation
7. Abstraction: predicate and variable abstraction, three-valued abstractions
8. Modular analysis via games
9. Overview of software verification
10. One of:
    • Models of timed systems
    • Models of Hybrid systems

Assignments

1. Modeling a simple system
2. Using invariant verification
3. Implementing verification algorithms using BDDs
4. Modeling Open Systems
5. Modeling Timed Systems