Schedule for Spring 2007

• Introduction, registration to course, course requirements

• Distribution of Home Assignment 1
• Systems and Software Verification: Automata; Chapter 1.1-1.4, pages 5-14 [Hyvärinen]
• Systems and Software Verification: Synchronization; Chapter 1.5-1.7, pages 14-26 [Korpela]

• Systems and Software Verification: Temporal Logics; Chapter 2-2.1, pages 27-32 [Halonen]
• Model Checking: Temporal Logics; Chapter 3-3.2, pages 27-32 [Kähkönen]

• Systems and Software Verification: Introduction to Temporal Logic Properties, Reachability, Deadlock-freeness; Part II Introduction, Chapters 6 and 9, pages 77-81, 99-101 [Häkkinen]
• Systems and Software Verification: Safety; Chapter 7, pages 83-89

• Deadline (at 16.15) for Home Assignment 1, Distribution of Home Assignment 2
• Systems and Software Verification: Liveness; Chapter 8, pages 91-98 [Pitkämäki]
• Systems and Software Verification: Fairness; Chapter 10, pages 103-107 [Bachmayer]
• Tutorial: Solutions to Home Assignment 1

• No seminar

• The Temporal Logic of Reactive and Concurrent Systems: Past Linear Time Temporal Logic, The Classification of Properties: Safety, Guarantee, Obligation, pages 192-201, 281-288 [Kähkönen]

• Deadline (at 16.15) for Home Assignment 2
• No seminar (examination week)

• Distribution of Home Assignment 3
• The Temporal Logic of Reactive and Concurrent Systems: The Classification of Properties: Response, Persistence, Reactivity, Standard Formulas, pages 288-302 [Halonen]
• Model Checking: CTL Model Checking; Chapter 4-4.1, pages 35-39
• Tutorial: Solutions to Home Assignment 2

• Model Checking: Fair CTL Model Checking, CTL* Model Checking; Chapter 3.3, 4.1.1, pages 32-33, 40-41, 46-49 [Launiainen]
• Model Checking: Büchi Automata; Chapter 9-9.2.1, pages 121-128 [Pitkämäki]

• Model Checking: Emptiness Checking of Automata, On-the-Fly Model Checking; Chapter 9.3, 9.5, pages 129-132, 138-139 [Häkkinen]

• Deadline (at 16.15) for Home Assignment 3, Distribution of Home Assignment 4
• Model Checking: Generalized Büchi Automata; Chapter 9.2.2, pages 128-129 + P. Wolper: Constructing Automata from Temporal Logic Formulas: A Tutorial [Korpela]
• Model Checking: Partial Order Reduction; Chapter 10-10.2, pages 141-147 [Bachmayer]
• Tutorial: Solutions to Home Assignment 3

• No seminar (Easter holiday)

• Systems and Software Verification: Abstraction; Chapter 11, pages 109-123 [Hyvärinen]
• Model Checking: Partial Order Reduction for LTL_-X; Chapter 10.3-10.4, pages 147-154

• Deadline (at 16.15) for Home Assignment 4
• Model Checking: Calculating Ample Sets, Heuristics, On-the-Fly Reduction; Chapter 10.5, pages 154-160 [Launiainen]
• Model Checking: Correctness of Partial Order Reduction, Partial Order Reduction in SPIN; Chapter 10.6-10.7, pages 160-170
• Tutorial: Solutions to Home Assignment 4