Schedule for Spring 2008

• Introduction, course arrangements

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

• Systems and Software Verification: Temporal Logics; Chapter 2-2.1, pages 27-32 [Osmo Turkulainen]
• Model Checking: Temporal Logics; Chapter 3-3.2, pages 27-32
• The Temporal Logic of Reactive and Concurrent Systems: Past Linear Time Temporal Logic; Chapter 3.3, pages 192-201

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

• No seminar

• Deadline (at 16:15) for Home Assignment 1
• Systems and Software Verification: Liveness; Chapter 8, pages 91-98 [Siert Wieringa]
• Systems and Software Verification: Fairness; Chapter 10, pages 103-107
• Tutorial: Solutions to Home Assignment 1

• Distribution of Home Assignment 2
• The Temporal Logic of Reactive and Concurrent Systems: The Classification of Properties: Safety, Guarantee, Obligation, pages 281-288
• The Temporal Logic of Reactive and Concurrent Systems: The Classification of Properties: Response, Persistence, Reactivity, Standard Formulas, pages 288-296, 298-302

• No seminar (examination week)

• Model Checking: CTL Model Checking; Chapter 4-4.1, pages 35-39 [Osmo Turkulainen]
• Model Checking: Büchi Automata; Chapter 9-9.2.1, pages 121-128

• No seminar (Easter holiday)

• Deadline (at 16:15) for Home Assignment 2
• Model Checking: Emptiness Checking of Automata, On-the-Fly Model Checking; Chapter 9.3, 9.5, pages 129-132, 138-139 [Yang Qiu]
• Tutorial: Solutions to Home Assignment 2

• Distribution of Home Assignment 3
• Model Checking: Generalized Büchi Automata; Chapter 9.2.2, pages 128-129 + P. Wolper: Constructing Automata from Temporal Logic Formulas: A Tutorial
• Model Checking: Fair CTL Model Checking, CTL* Model Checking; Chapter 3.3, 4.1.1, pages 32-33, 40-41, 46-49

• Model Checking: Partial Order Reduction; Chapter 10-10.2, pages 141-147 [Siert Wieringa]
• Model Checking: Partial Order Reduction for LTL_-X; Chapter 10.3-10.4, pages 147-154

• Model Checking: Calculating Ample Sets, Heuristics, On-the-Fly Reduction; Chapter 10.5, pages 154-160
• Model Checking: Correctness of Partial Order Reduction, Partial Order Reduction in SPIN; Chapter 10.6-10.7, pages 160-170

• G. J. Holzmann, M. H. Smith: An automated verification method for distributed systems software based on model extraction [Osmo Turkulainen]
• P. Godefroid: Software model checking: The VeriSoft approach [Yang Qiu]

• Deadline (at 16:15) for Home Assignment 3
• J. Barnat, I. Černá: Distributed breadth-first search LTL model checking [Siert Wieringa]
• Tutorial: Solutions to Home Assignment 3