Tue Jan 22

- Introduction, course arrangements

Tue Jan 29

- 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

Tue Feb 5

- 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

Tue Feb 12

- 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

Tue Feb 19

- No seminar

Tue Feb 26

- 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

Tue Mar 4

- 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

Tue Mar 11

- No seminar (examination week)

Tue Mar 18

- 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

Tue Mar 25

- No seminar (Easter holiday)

Tue Apr 1

- 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

Tue Apr 8

- 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

Tue Apr 15

- 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

Tue Apr 22

- 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

Tue Apr 29

- 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]

Tue May 6

- 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

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]

Latest update: 23 April 2008.