Model Checking

Week 1: Modeling systems as Finite-state machines
Week 2: Using the model-checker NuSMV
Week 3: Linear-time properties for verification
Week 4: Regular properties – automata over finite words
Week 5: Omega-regular properties – automata over infinite words
Week 6: Model checking omega-regular properties
Week 7: Linear Temporal Logic (LTL)
Week 8: Algorithms for LTL
Week 9: Computation Tree Logic (CTL)
Week 10: Algorithms for CTL
Week 11: Binary Decision Diagrams (BDDs)
Week 12: Models with timing constraints – timed automataRegular properties – automata over finite words